| 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 374 | . . 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 206 |
| 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 207 |
| This theorem is referenced by: pm5.21nd 802 sbcrext 3873 rmob 3890 elpr2g 4651 oteqex 5505 epelg 5585 eqbrrdva 5880 relbrcnvg 6123 ordsucuniel 7844 ordsucun 7845 xpord2pred 8170 brtpos2 8257 eceqoveq 8862 elpmg 8883 elfi2 9454 brwdom 9607 brwdomn0 9609 rankr1c 9861 r1pwcl 9887 ttukeylem1 10549 fpwwe2lem8 10678 eltskm 10883 recmulnq 11004 clim 15530 rlim 15531 lo1o1 15568 o1lo1 15573 o1lo12 15574 rlimresb 15601 lo1eq 15604 rlimeq 15605 isercolllem2 15702 caucvgb 15716 saddisj 16502 sadadd 16504 sadass 16508 bitsshft 16512 smupvallem 16520 smumul 16530 catpropd 17752 isssc 17864 issubc 17880 funcres2b 17942 funcres2c 17948 sgrppropd 18744 mndpropd 18772 issubg3 19162 resghm2b 19252 resscntz 19351 elsymgbas 19391 odmulg 19574 dmdprd 20018 dprdw 20030 subgdmdprd 20054 lmodprop2d 20922 lssacs 20965 prmirred 21485 lindfmm 21847 lsslindf 21850 islinds3 21854 assapropd 21892 psrbaglefi 21946 cnrest2 23294 cnprest 23297 cnprest2 23298 lmss 23306 isfildlem 23865 isfcls 24017 elutop 24242 metustel 24563 blval2 24575 dscopn 24586 iscau2 25311 causs 25332 ismbf 25663 ismbfcn 25664 iblcnlem 25824 limcdif 25911 limcres 25921 limcun 25930 dvres 25946 q1peqb 26195 ulmval 26423 ulmres 26431 chpchtsum 27263 dchrisum0lem1 27560 elmade 27906 axcontlem5 28983 iswlkg 29631 issiga 34113 ismeas 34200 elcarsg 34307 cvmlift3lem4 35327 msrrcl 35548 brcolinear2 36059 topfneec 36356 bj-epelg 37069 cnpwstotbnd 37804 ismtyima 37810 ismndo2 37881 isrngo 37904 lshpkr 39118 fimgmcyc 42544 elrfi 42705 traxext 44994 climf 45637 climf2 45681 isupwlkg 48053 |
| Copyright terms: Public domain | W3C validator |