![]() |
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 376 | . 2 ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒)) |
5 | 1, 4 | pm2.61i 182 | 1 ⊢ (𝜑 ↔ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → 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: clelab 2871 elrabf 3675 elrab 3679 sbccow 3796 sbcco 3799 sbc5ALT 3802 sbcan 3826 sbcor 3827 sbcal 3837 sbcex2 3838 sbcel1v 3844 sbcreu 3866 eldif 3954 elin 3960 elun 4145 sbccsb2 4436 2reu4 4528 eluni 4912 eliun 5001 sbcbr123 5203 elopab 5529 opelopabsb 5532 opeliunxp2 5841 inisegn0 6103 brfvopabrbr 7001 elpwun 7772 elxp5 7931 opeliunxp2f 8216 tpostpos 8252 ecdmn0 8773 brecop2 8830 elixpsn 8956 bren 8974 brenOLD 8975 0sdom1dom 9266 elharval 9591 brttrcl 9743 sdom2en01 10332 isfin1-2 10415 wdomac 10557 elwina 10716 elina 10717 lterpq 11000 ltrnq 11009 elnp 11017 elnpi 11018 ltresr 11170 eluz2 12866 dfle2 13166 dflt2 13167 rexanuz2 15340 even2n 16330 isstruct2 17137 xpsfrnel2 17565 ismre 17589 isacs 17650 brssc 17816 isfunc 17869 oduclatb 18518 isipodrs 18548 issubg 19106 isnsg 19135 oppgsubm 19345 oppgsubg 19346 isslw 19592 efgrelexlema 19733 dvdsr 20330 isunit 20341 isirred 20387 isrim0 20451 issubrng 20513 opprsubrng 20525 issubrg 20539 opprsubrg 20561 islss 20847 islbs4 21800 istopon 22875 basdif0 22917 dis2ndc 23425 elmptrab 23792 isusp 24227 ismet2 24300 isphtpc 24981 elpi1 25033 iscmet 25273 bcthlem1 25313 elno 27644 elnoOLD 27645 wlkcpr 29535 isvcOLD 30481 isnv 30514 hlimi 31090 h1de2ci 31458 elunop 31774 ispcmp 33609 elmpps 35334 eldm3 35506 opelco3 35521 elima4 35522 brsset 35636 brbigcup 35645 elfix2 35651 elsingles 35665 imageval 35677 funpartlem 35689 elaltxp 35722 ellines 35899 isfne4 35975 bj-ismoore 36735 bj-idreseqb 36793 istotbnd 37393 isbnd 37404 isdrngo1 37580 elrab2w 42232 isnacs 42271 sbccomieg 42360 elmnc 42707 ismea 45982 |
Copyright terms: Public domain | W3C validator |