| 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 377 | . 2 ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒)) |
| 5 | 1, 4 | pm2.61i 182 | 1 ⊢ (𝜑 ↔ 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: → 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: clelab 2887 elrabf 3688 elrab 3692 elrab2w 3696 sbccow 3811 sbcco 3814 sbc5ALT 3817 sbcan 3838 sbcor 3839 sbcal 3849 sbcex2 3850 sbcel1v 3856 sbcreu 3876 eldif 3961 elin 3967 elun 4153 sbccsb2 4437 2reu4 4523 eluni 4910 eliun 4995 sbcbr123 5197 elopab 5532 opelopabsb 5535 opeliunxp2 5849 inisegn0 6116 brfvopabrbr 7013 elpwun 7789 elxp5 7945 opeliunxp2f 8235 tpostpos 8271 ecdmn0 8794 brecop2 8851 elixpsn 8977 bren 8995 0sdom1dom 9274 elharval 9601 brttrcl 9753 sdom2en01 10342 isfin1-2 10425 wdomac 10567 elwina 10726 elina 10727 lterpq 11010 ltrnq 11019 elnp 11027 elnpi 11028 ltresr 11180 eluz2 12884 dfle2 13189 dflt2 13190 rexanuz2 15388 even2n 16379 isstruct2 17186 xpsfrnel2 17609 ismre 17633 isacs 17694 brssc 17858 isfunc 17909 oduclatb 18552 isipodrs 18582 issubg 19144 isnsg 19173 oppgsubm 19381 oppgsubg 19382 isslw 19626 efgrelexlema 19767 dvdsr 20362 isunit 20373 isirred 20419 isrim0 20483 issubrng 20547 opprsubrng 20559 issubrg 20571 opprsubrg 20593 islss 20932 islbs4 21852 istopon 22918 basdif0 22960 dis2ndc 23468 elmptrab 23835 isusp 24270 ismet2 24343 isphtpc 25026 elpi1 25078 iscmet 25318 bcthlem1 25358 elno 27690 elnoOLD 27691 elzs12 28421 wlkcpr 29647 isvcOLD 30598 isnv 30631 hlimi 31207 h1de2ci 31575 elunop 31891 ispcmp 33856 elmpps 35578 eldm3 35761 opelco3 35775 elima4 35776 brsset 35890 brbigcup 35899 elfix2 35905 elsingles 35919 imageval 35931 funpartlem 35943 elaltxp 35976 ellines 36153 isfne4 36341 bj-ismoore 37106 bj-idreseqb 37164 istotbnd 37776 isbnd 37787 isdrngo1 37963 isnacs 42715 sbccomieg 42804 elmnc 43148 ismea 46466 |
| Copyright terms: Public domain | W3C validator |