Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm5.21ndd | Structured version Visualization version GIF version |
Description: Eliminate an antecedent implied by each side of a biconditional, deduction version. (Contributed by Paul Chapman, 21-Nov-2012.) (Proof shortened by Wolf Lammen, 6-Oct-2013.) |
Ref | Expression |
---|---|
pm5.21ndd.1 | ⊢ (𝜑 → (𝜒 → 𝜓)) |
pm5.21ndd.2 | ⊢ (𝜑 → (𝜃 → 𝜓)) |
pm5.21ndd.3 | ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) |
Ref | Expression |
---|---|
pm5.21ndd | ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.21ndd.3 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) | |
2 | pm5.21ndd.1 | . . . 4 ⊢ (𝜑 → (𝜒 → 𝜓)) | |
3 | 2 | con3d 155 | . . 3 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒)) |
4 | pm5.21ndd.2 | . . . 4 ⊢ (𝜑 → (𝜃 → 𝜓)) | |
5 | 4 | con3d 155 | . . 3 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜃)) |
6 | pm5.21im 378 | . . 3 ⊢ (¬ 𝜒 → (¬ 𝜃 → (𝜒 ↔ 𝜃))) | |
7 | 3, 5, 6 | syl6c 70 | . 2 ⊢ (𝜑 → (¬ 𝜓 → (𝜒 ↔ 𝜃))) |
8 | 1, 7 | pm2.61d 182 | 1 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 210 |
This theorem is referenced by: pm5.21nd 802 sbcrext 3776 rmob 3793 elpr2g 4555 oteqex 5372 epelg 5450 eqbrrdva 5727 relbrcnvg 5962 ordsucuniel 7592 ordsucun 7593 brtpos2 7963 eceqoveq 8493 elpmg 8513 elfi2 9019 brwdom 9172 brwdomn0 9174 rankr1c 9420 r1pwcl 9446 ttukeylem1 10106 fpwwe2lem8 10235 eltskm 10440 recmulnq 10561 clim 15038 rlim 15039 lo1o1 15076 o1lo1 15081 o1lo12 15082 rlimresb 15109 lo1eq 15112 rlimeq 15113 isercolllem2 15212 caucvgb 15226 saddisj 16005 sadadd 16007 sadass 16011 bitsshft 16015 smupvallem 16023 smumul 16033 catpropd 17184 isssc 17297 issubc 17313 funcres2b 17375 funcres2c 17380 mndpropd 18170 issubg3 18533 resghm2b 18612 resscntz 18698 elsymgbas 18738 odmulg 18919 dmdprd 19357 dprdw 19369 subgdmdprd 19393 lmodprop2d 19933 lssacs 19976 prmirred 20433 lindfmm 20761 lsslindf 20764 islinds3 20768 assapropd 20803 psrbaglefi 20863 psrbaglefiOLD 20864 cnrest2 22155 cnprest 22158 cnprest2 22159 lmss 22167 isfildlem 22726 isfcls 22878 elutop 23103 metustel 23420 blval2 23432 dscopn 23443 iscau2 24146 causs 24167 ismbf 24497 ismbfcn 24498 iblcnlem 24658 limcdif 24745 limcres 24755 limcun 24764 dvres 24780 q1peqb 25024 ulmval 25244 ulmres 25252 chpchtsum 26072 dchrisum0lem1 26369 axcontlem5 27031 iswlkg 27673 issiga 31764 ismeas 31851 elcarsg 31956 cvmlift3lem4 32969 msrrcl 33190 xpord2pred 33480 elmade 33745 brcolinear2 34054 topfneec 34238 bj-epelg 34932 cnpwstotbnd 35649 ismtyima 35655 ismndo2 35726 isrngo 35749 lshpkr 36825 elrfi 40171 climf 42792 climf2 42836 isupwlkg 44926 |
Copyright terms: Public domain | W3C validator |