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 376 | . . 3 ⊢ (¬ 𝜒 → (¬ 𝜃 → (𝜒 ↔ 𝜃))) | |
7 | 3, 5, 6 | syl6c 70 | . 2 ⊢ (𝜑 → (¬ 𝜓 → (𝜒 ↔ 𝜃))) |
8 | 1, 7 | pm2.61d 180 | 1 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 |
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 208 |
This theorem is referenced by: pm5.21nd 798 sbcrext 3855 rmob 3873 oteqex 5382 epelg 5460 epelgOLD 5461 eqbrrdva 5734 relbrcnvg 5962 ordsucuniel 7527 ordsucun 7528 brtpos2 7889 eceqoveq 8392 elpmg 8412 elfi2 8867 brwdom 9020 brwdomn0 9022 rankr1c 9239 r1pwcl 9265 ttukeylem1 9920 fpwwe2lem9 10049 eltskm 10254 recmulnq 10375 clim 14841 rlim 14842 lo1o1 14879 o1lo1 14884 o1lo12 14885 rlimresb 14912 lo1eq 14915 rlimeq 14916 isercolllem2 15012 caucvgb 15026 saddisj 15804 sadadd 15806 sadass 15810 bitsshft 15814 smupvallem 15822 smumul 15832 catpropd 16969 isssc 17080 issubc 17095 funcres2b 17157 funcres2c 17161 mndpropd 17926 issubg3 18237 resghm2b 18316 resscntz 18402 elsymgbas 18440 odmulg 18614 dmdprd 19051 dprdw 19063 subgdmdprd 19087 lmodprop2d 19627 lssacs 19670 assapropd 20031 psrbaglefi 20082 prmirred 20572 lindfmm 20901 lsslindf 20904 islinds3 20908 cnrest2 21824 cnprest 21827 cnprest2 21828 lmss 21836 isfildlem 22395 isfcls 22547 elutop 22771 metustel 23089 blval2 23101 dscopn 23112 iscau2 23809 causs 23830 ismbf 24158 ismbfcn 24159 iblcnlem 24318 limcdif 24403 limcres 24413 limcun 24422 dvres 24438 q1peqb 24677 ulmval 24897 ulmres 24905 chpchtsum 25723 dchrisum0lem1 26020 axcontlem5 26682 iswlkg 27323 issiga 31271 ismeas 31358 elcarsg 31463 cvmlift3lem4 32467 msrrcl 32688 brcolinear2 33417 topfneec 33601 bj-epelg 34255 cnpwstotbnd 34958 ismtyima 34964 ismndo2 35035 isrngo 35058 lshpkr 36135 elrfi 39171 climf 41783 climf2 41827 isupwlkg 43859 |
Copyright terms: Public domain | W3C validator |