![]() |
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 152 | . . 3 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒)) |
4 | pm5.21ndd.2 | . . . 4 ⊢ (𝜑 → (𝜃 → 𝜓)) | |
5 | 4 | con3d 152 | . . 3 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜃)) |
6 | pm5.21im 373 | . . 3 ⊢ (¬ 𝜒 → (¬ 𝜃 → (𝜒 ↔ 𝜃))) | |
7 | 3, 5, 6 | syl6c 70 | . 2 ⊢ (𝜑 → (¬ 𝜓 → (𝜒 ↔ 𝜃))) |
8 | 1, 7 | pm2.61d 179 | 1 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: pm5.21nd 800 sbcrext 3868 rmob 3885 elpr2g 4657 oteqex 5506 epelg 5587 eqbrrdva 5876 relbrcnvg 6114 ordsucuniel 7833 ordsucun 7834 xpord2pred 8156 brtpos2 8244 eceqoveq 8847 elpmg 8868 elfi2 9445 brwdom 9598 brwdomn0 9600 rankr1c 9852 r1pwcl 9878 ttukeylem1 10540 fpwwe2lem8 10669 eltskm 10874 recmulnq 10995 clim 15478 rlim 15479 lo1o1 15516 o1lo1 15521 o1lo12 15522 rlimresb 15549 lo1eq 15552 rlimeq 15553 isercolllem2 15652 caucvgb 15666 saddisj 16447 sadadd 16449 sadass 16453 bitsshft 16457 smupvallem 16465 smumul 16475 catpropd 17696 isssc 17810 issubc 17828 funcres2b 17890 funcres2c 17897 sgrppropd 18698 mndpropd 18726 issubg3 19106 resghm2b 19195 resscntz 19291 elsymgbas 19335 odmulg 19518 dmdprd 19962 dprdw 19974 subgdmdprd 19998 lmodprop2d 20814 lssacs 20858 prmirred 21407 lindfmm 21768 lsslindf 21771 islinds3 21775 assapropd 21812 psrbaglefi 21872 psrbaglefiOLD 21873 cnrest2 23210 cnprest 23213 cnprest2 23214 lmss 23222 isfildlem 23781 isfcls 23933 elutop 24158 metustel 24479 blval2 24491 dscopn 24502 iscau2 25225 causs 25246 ismbf 25577 ismbfcn 25578 iblcnlem 25738 limcdif 25825 limcres 25835 limcun 25844 dvres 25860 q1peqb 26111 ulmval 26336 ulmres 26344 chpchtsum 27172 dchrisum0lem1 27469 elmade 27814 axcontlem5 28799 iswlkg 29447 issiga 33764 ismeas 33851 elcarsg 33958 cvmlift3lem4 34965 msrrcl 35186 brcolinear2 35687 topfneec 35872 bj-epelg 36580 cnpwstotbnd 37303 ismtyima 37309 ismndo2 37380 isrngo 37403 lshpkr 38621 elrfi 42145 climf 45039 climf2 45083 isupwlkg 47277 |
Copyright terms: Public domain | W3C validator |