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 147 | . . 3 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒)) |
4 | pm5.21ndd.2 | . . . 4 ⊢ (𝜑 → (𝜃 → 𝜓)) | |
5 | 4 | con3d 147 | . . 3 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜃)) |
6 | pm5.21im 363 | . . 3 ⊢ (¬ 𝜒 → (¬ 𝜃 → (𝜒 ↔ 𝜃))) | |
7 | 3, 5, 6 | syl6c 68 | . 2 ⊢ (𝜑 → (¬ 𝜓 → (𝜒 ↔ 𝜃))) |
8 | 1, 7 | pm2.61d 169 | 1 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 |
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 196 |
This theorem is referenced by: pm5.21nd 939 sbcrext 3478 rmob 3495 oteqex 4889 epelg 4950 eqbrrdva 5213 relbrcnvg 5423 ordsucuniel 6916 ordsucun 6917 brtpos2 7245 eceqoveq 7740 elpmg 7759 elfi2 8203 brwdom 8355 brwdomn0 8357 rankr1c 8567 r1pwcl 8593 ttukeylem1 9214 fpwwe2lem9 9339 eltskm 9544 recmulnq 9665 clim 14073 rlim 14074 lo1o1 14111 o1lo1 14116 o1lo12 14117 rlimresb 14144 lo1eq 14147 rlimeq 14148 isercolllem2 14244 caucvgb 14258 saddisj 15025 sadadd 15027 sadass 15031 bitsshft 15035 smupvallem 15043 smumul 15053 catpropd 16192 isssc 16303 issubc 16318 funcres2b 16380 funcres2c 16384 mndpropd 17139 issubg3 17435 resghm2b 17501 resscntz 17587 elsymgbas 17625 odmulg 17796 dmdprd 18220 dprdw 18232 subgdmdprd 18256 lmodprop2d 18748 lssacs 18788 assapropd 19148 psrbaglefi 19193 prmirred 19662 lindfmm 19985 lsslindf 19988 islinds3 19992 cnrest2 20900 cnprest 20903 cnprest2 20904 lmss 20912 isfildlem 21471 isfcls 21623 elutop 21847 metustel 22165 blval2 22177 dscopn 22188 iscau2 22883 causs 22904 ismbf 23203 ismbfcn 23204 iblcnlem 23361 limcdif 23446 limcres 23456 limcun 23465 dvres 23481 q1peqb 23718 ulmval 23938 ulmres 23946 chpchtsum 24744 dchrisum0lem1 25005 axcontlem5 25648 iseupa 26492 issiga 29501 ismeas 29589 elcarsg 29694 cvmlift3lem4 30558 msrrcl 30694 brcolinear2 31335 topfneec 31520 cnpwstotbnd 32766 ismtyima 32772 ismndo2 32843 isrngo 32866 lshpkr 33422 elrfi 36275 climf 38689 climf2 38733 is1wlkg 40816 |
Copyright terms: Public domain | W3C validator |