![]() |
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 3790 rmob 3808 oteqex 5288 epelg 5361 epelgOLD 5362 eqbrrdva 5633 relbrcnvg 5851 ordsucuniel 7402 ordsucun 7403 brtpos2 7756 eceqoveq 8259 elpmg 8279 elfi2 8731 brwdom 8884 brwdomn0 8886 rankr1c 9103 r1pwcl 9129 ttukeylem1 9784 fpwwe2lem9 9913 eltskm 10118 recmulnq 10239 clim 14689 rlim 14690 lo1o1 14727 o1lo1 14732 o1lo12 14733 rlimresb 14760 lo1eq 14763 rlimeq 14764 isercolllem2 14860 caucvgb 14874 saddisj 15651 sadadd 15653 sadass 15657 bitsshft 15661 smupvallem 15669 smumul 15679 catpropd 16812 isssc 16923 issubc 16938 funcres2b 17000 funcres2c 17004 mndpropd 17759 issubg3 18055 resghm2b 18121 resscntz 18207 elsymgbas 18245 odmulg 18417 dmdprd 18841 dprdw 18853 subgdmdprd 18877 lmodprop2d 19390 lssacs 19433 assapropd 19793 psrbaglefi 19844 prmirred 20328 lindfmm 20657 lsslindf 20660 islinds3 20664 cnrest2 21582 cnprest 21585 cnprest2 21586 lmss 21594 isfildlem 22153 isfcls 22305 elutop 22529 metustel 22847 blval2 22859 dscopn 22870 iscau2 23567 causs 23588 ismbf 23916 ismbfcn 23917 iblcnlem 24076 limcdif 24161 limcres 24171 limcun 24180 dvres 24196 q1peqb 24435 ulmval 24655 ulmres 24663 chpchtsum 25481 dchrisum0lem1 25778 axcontlem5 26441 iswlkg 27082 issiga 30984 ismeas 31071 elcarsg 31176 cvmlift3lem4 32179 msrrcl 32400 brcolinear2 33130 topfneec 33314 cnpwstotbnd 34628 ismtyima 34634 ismndo2 34705 isrngo 34728 lshpkr 35805 elrfi 38797 climf 41466 climf2 41510 isupwlkg 43516 |
Copyright terms: Public domain | W3C validator |