Metamath Proof Explorer


Theorem cdlemd5

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 30-May-2012)

Ref Expression
Hypotheses cdlemd4.l ˙=K
cdlemd4.j ˙=joinK
cdlemd4.a A=AtomsK
cdlemd4.h H=LHypK
cdlemd4.t T=LTrnKW
Assertion cdlemd5 KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQFR=GR

Proof

Step Hyp Ref Expression
1 cdlemd4.l ˙=K
2 cdlemd4.j ˙=joinK
3 cdlemd4.a A=AtomsK
4 cdlemd4.h H=LHypK
5 cdlemd4.t T=LTrnKW
6 fveq2 R=PFR=FP
7 fveq2 R=PGR=GP
8 6 7 eqeq12d R=PFR=GRFP=GP
9 simpll1 KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQR˙P˙QRPKHLWHFTGTRA
10 simpl21 KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQR˙P˙QPA¬P˙W
11 10 adantr KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQR˙P˙QRPPA¬P˙W
12 simpl22 KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQR˙P˙QQA¬Q˙W
13 12 adantr KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQR˙P˙QRPQA¬Q˙W
14 simp23 KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQPQ
15 14 ad2antrr KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQR˙P˙QRPPQ
16 simplr KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQR˙P˙QRPR˙P˙Q
17 simpr KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQR˙P˙QRPRP
18 15 16 17 3jca KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQR˙P˙QRPPQR˙P˙QRP
19 simpll3 KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQR˙P˙QRPFP=GPFQ=GQ
20 1 2 3 4 5 cdlemd4 KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQR˙P˙QRPFP=GPFQ=GQFR=GR
21 9 11 13 18 19 20 syl131anc KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQR˙P˙QRPFR=GR
22 simpl3l KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQR˙P˙QFP=GP
23 8 21 22 pm2.61ne KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQR˙P˙QFR=GR
24 simpl1 KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQ¬R˙P˙QKHLWHFTGTRA
25 simpl21 KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQ¬R˙P˙QPA¬P˙W
26 simpl22 KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQ¬R˙P˙QQA¬Q˙W
27 simpl23 KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQ¬R˙P˙QPQ
28 simpr KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQ¬R˙P˙Q¬R˙P˙Q
29 27 28 jca KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQ¬R˙P˙QPQ¬R˙P˙Q
30 simpl3 KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQ¬R˙P˙QFP=GPFQ=GQ
31 1 2 3 4 5 cdlemd2 KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQ¬R˙P˙QFP=GPFQ=GQFR=GR
32 24 25 26 29 30 31 syl131anc KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQ¬R˙P˙QFR=GR
33 23 32 pm2.61dan KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQFR=GR