Theorem pm5.21nii 378

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

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