![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm5.21nii | Structured version Visualization version GIF version |
Description: Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.) |
Ref | Expression |
---|---|
pm5.21ni.1 | ⊢ (𝜑 → 𝜓) |
pm5.21ni.2 | ⊢ (𝜒 → 𝜓) |
pm5.21nii.3 | ⊢ (𝜓 → (𝜑 ↔ 𝜒)) |
Ref | Expression |
---|---|
pm5.21nii | ⊢ (𝜑 ↔ 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.21nii.3 | . 2 ⊢ (𝜓 → (𝜑 ↔ 𝜒)) | |
2 | pm5.21ni.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
3 | pm5.21ni.2 | . . 3 ⊢ (𝜒 → 𝜓) | |
4 | 2, 3 | pm5.21ni 370 | . 2 ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒)) |
5 | 1, 4 | pm2.61i 177 | 1 ⊢ (𝜑 ↔ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 |
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 199 |
This theorem is referenced by: elrabf 3586 elrab 3590 sbcco 3699 sbc5 3701 sbcan 3720 sbcor 3721 sbcal 3731 sbcex2 3732 sbcel1v 3737 sbcel1vOLD 3738 sbcreu 3757 eldif 3834 elun 4009 elin 4052 sbccsb2 4265 2reu4 4344 elpr2 4460 eluni 4712 eliun 4793 sbcbr123 4980 elopab 5266 opelopabsb 5268 opeliunxp2 5556 inisegn0 5799 brfvopabrbr 6591 elpwun 7307 elxp5 7442 opeliunxp2f 7678 tpostpos 7714 ecdmn0 8135 brecop2 8190 elixpsn 8297 bren 8314 elharval 8821 sdom2en01 9521 isfin1-2 9604 wdomac 9746 elwina 9905 elina 9906 lterpq 10189 ltrnq 10198 elnp 10206 elnpi 10207 ltresr 10359 eluz2 12063 dfle2 12356 dflt2 12357 rexanuz2 14569 even2n 15550 isstruct2 16348 xpsfrnel2cda 16699 xpsfrnel2 16702 ismre 16732 isacs 16793 brssc 16955 isfunc 17005 oduclatb 17625 isipodrs 17642 issubg 18076 isnsg 18105 oppgsubm 18274 oppgsubg 18275 isslw 18507 efgrelexlema 18648 dvdsr 19132 isunit 19143 isirred 19185 issubrg 19271 opprsubrg 19292 islss 19441 islbs4 20694 istopon 21240 basdif0 21281 dis2ndc 21788 elmptrab 22155 isusp 22589 ismet2 22662 isphtpc 23317 elpi1 23368 iscmet 23606 bcthlem1 23646 wlkcpr 27129 frgrusgrfrcond 27809 isvcOLD 28149 isnv 28182 hlimi 28760 h1de2ci 29130 elunop 29446 ispcmp 30798 elmpps 32373 eldm3 32550 opelco3 32571 elima4 32572 elno 32707 brsset 32904 brbigcup 32913 elfix2 32919 elsingles 32933 imageval 32945 funpartlem 32957 elaltxp 32990 ellines 33167 isfne4 33242 istotbnd 34522 isbnd 34533 isdrngo1 34709 isnacs 38730 sbccomieg 38820 elmnc 39166 ismea 42194 |
Copyright terms: Public domain | W3C validator |