Theorem pm5.21nii 380

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 379	. 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  2881  elrabf  3633  elrab  3637  sbccow  3753  sbcco  3756  sbc5ALT  3759  sbcan  3782  sbcor  3783  sbcal  3794  sbcex2  3795  sbcel1v  3801  sbcreu  3823  eldif  3911  elin  3917  elun  4099  sbccsb2  4385  2reu4  4475  elpr2OLD  4603  eluni  4859  eliun  4949  sbcbr123  5150  elopab  5475  opelopabsb  5478  opeliunxp2  5784  inisegn0  6040  brfvopabrbr  6932  elpwun  7685  elxp5  7842  opeliunxp2f  8100  tpostpos  8136  ecdmn0  8620  brecop2  8675  elixpsn  8800  bren  8818  brenOLD  8819  0sdom1dom  9107  elharval  9422  brttrcl  9574  sdom2en01  10163  isfin1-2  10246  wdomac  10388  elwina  10547  elina  10548  lterpq  10831  ltrnq  10840  elnp  10848  elnpi  10849  ltresr  11001  eluz2  12693  dfle2  12986  dflt2  12987  rexanuz2  15160  even2n  16150  isstruct2  16947  xpsfrnel2  17372  ismre  17396  isacs  17457  brssc  17623  isfunc  17676  oduclatb  18322  isipodrs  18352  issubg  18851  isnsg  18879  oppgsubm  19065  oppgsubg  19066  isslw  19309  efgrelexlema  19450  dvdsr  19982  isunit  19993  isirred  20035  isrim0  20063  issubrg  20128  opprsubrg  20149  islss  20301  islbs4  21144  istopon  22166  basdif0  22208  dis2ndc  22716  elmptrab  23083  isusp  23518  ismet2  23591  isphtpc  24262  elpi1  24313  iscmet  24553  bcthlem1  24593  elno  26899  wlkcpr  28284  isvcOLD  29228  isnv  29261  hlimi  29837  h1de2ci  30205  elunop  30521  ispcmp  32103  elmpps  33832  eldm3  34017  opelco3  34032  elima4  34033  brsset  34328  brbigcup  34337  elfix2  34343  elsingles  34357  imageval  34369  funpartlem  34381  elaltxp  34414  ellines  34591  isfne4  34666  bj-ismoore  35430  bj-idreseqb  35488  istotbnd  36083  isbnd  36094  isdrngo1  36270  elrab2w  40475  isnacs  40839  sbccomieg  40928  elmnc  41275  ismea  44378