Theorem pm5.21nii 379

Description: Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.)

Hypotheses

Ref	Expression
pm5.21ni.1	⊢ (𝜑 → 𝜓)
pm5.21ni.2	⊢ (𝜒 → 𝜓)
pm5.21nii.3	⊢ (𝜓 → (𝜑 ↔ 𝜒))

Assertion

Ref	Expression
pm5.21nii	⊢ (𝜑 ↔ 𝜒)

Proof of Theorem 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 378	. 2 ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒))
5	1, 4	pm2.61i 182	1 ⊢ (𝜑 ↔ 𝜒)

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  2878  elrabf  3644  elrab  3648  sbccow  3765  sbcco  3768  sbc5ALT  3771  sbcan  3794  sbcor  3795  sbcal  3806  sbcex2  3807  sbcel1v  3813  sbcreu  3835  eldif  3923  elin  3929  elun  4113  sbccsb2  4399  2reu4  4489  elpr2OLD  4617  eluni  4873  eliun  4963  sbcbr123  5164  elopab  5489  opelopabsb  5492  opeliunxp2  5799  inisegn0  6055  brfvopabrbr  6950  elpwun  7708  elxp5  7865  opeliunxp2f  8146  tpostpos  8182  ecdmn0  8702  brecop2  8757  elixpsn  8882  bren  8900  brenOLD  8901  0sdom1dom  9189  elharval  9506  brttrcl  9658  sdom2en01  10247  isfin1-2  10330  wdomac  10472  elwina  10631  elina  10632  lterpq  10915  ltrnq  10924  elnp  10932  elnpi  10933  ltresr  11085  eluz2  12778  dfle2  13076  dflt2  13077  rexanuz2  15246  even2n  16235  isstruct2  17032  xpsfrnel2  17460  ismre  17484  isacs  17545  brssc  17711  isfunc  17764  oduclatb  18410  isipodrs  18440  issubg  18942  isnsg  18971  oppgsubm  19157  oppgsubg  19158  isslw  19404  efgrelexlema  19545  dvdsr  20089  isunit  20100  isirred  20144  isrim0  20172  issubrg  20270  opprsubrg  20291  islss  20452  islbs4  21275  istopon  22298  basdif0  22340  dis2ndc  22848  elmptrab  23215  isusp  23650  ismet2  23723  isphtpc  24394  elpi1  24445  iscmet  24685  bcthlem1  24725  elno  27031  wlkcpr  28640  isvcOLD  29584  isnv  29617  hlimi  30193  h1de2ci  30561  elunop  30877  ispcmp  32527  elmpps  34254  eldm3  34420  opelco3  34435  elima4  34436  brsset  34550  brbigcup  34559  elfix2  34565  elsingles  34579  imageval  34591  funpartlem  34603  elaltxp  34636  ellines  34813  isfne4  34888  bj-ismoore  35649  bj-idreseqb  35707  istotbnd  36301  isbnd  36312  isdrngo1  36488  elrab2w  40692  isnacs  41085  sbccomieg  41174  elmnc  41521  ismea  44812