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  2882  elrabf  3613  elrab  3617  sbccow  3734  sbcco  3737  sbc5ALT  3740  sbcan  3763  sbcor  3764  sbcal  3776  sbcex2  3777  sbcel1v  3783  sbcreu  3805  eldif  3893  elin  3899  elun  4079  sbccsb2  4365  2reu4  4454  elpr2OLD  4584  eluni  4839  eliun  4925  sbcbr123  5124  elopab  5433  opelopabsb  5436  opeliunxp2  5736  inisegn0  5995  brfvopabrbr  6854  elpwun  7597  elxp5  7744  opeliunxp2f  7997  tpostpos  8033  ecdmn0  8503  brecop2  8558  elixpsn  8683  bren  8701  brenOLD  8702  elharval  9250  sdom2en01  9989  isfin1-2  10072  wdomac  10214  elwina  10373  elina  10374  lterpq  10657  ltrnq  10666  elnp  10674  elnpi  10675  ltresr  10827  eluz2  12517  dfle2  12810  dflt2  12811  rexanuz2  14989  even2n  15979  isstruct2  16778  xpsfrnel2  17192  ismre  17216  isacs  17277  brssc  17443  isfunc  17495  oduclatb  18140  isipodrs  18170  issubg  18670  isnsg  18698  oppgsubm  18884  oppgsubg  18885  isslw  19128  efgrelexlema  19270  dvdsr  19803  isunit  19814  isirred  19856  issubrg  19939  opprsubrg  19960  islss  20111  islbs4  20949  istopon  21969  basdif0  22011  dis2ndc  22519  elmptrab  22886  isusp  23321  ismet2  23394  isphtpc  24063  elpi1  24114  iscmet  24353  bcthlem1  24393  wlkcpr  27898  isvcOLD  28842  isnv  28875  hlimi  29451  h1de2ci  29819  elunop  30135  ispcmp  31709  elmpps  33435  eldm3  33634  opelco3  33655  elima4  33656  brttrcl  33699  elno  33776  brsset  34118  brbigcup  34127  elfix2  34133  elsingles  34147  imageval  34159  funpartlem  34171  elaltxp  34204  ellines  34381  isfne4  34456  bj-ismoore  35203  bj-idreseqb  35261  istotbnd  35854  isbnd  35865  isdrngo1  36041  elrab2w  40095  isnacs  40442  sbccomieg  40531  elmnc  40877  ismea  43879