Theorem pm5.21nii 381

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  clelab  2908  elrabf  3645  elrab  3648  elrab2w  3653  sbccow  3765  sbcco  3768  sbc5ALT  3771  sbcan  3791  sbcor  3792  sbcal  3801  sbcex2  3802  sbcel1v  3807  sbcfal  3816  sbcreu  3827  eldif  4052  elin  4096  elun  4155  sbccsb2  4398  2reu4  4483  eluni  4875  eliun  4960  sbcbr123  5166  elopab  5508  opelopabsb  5511  opeliunxp2  5825  inisegn0  6114  brfvopabrbr  7021  elpwun  7815  elxp5  7969  opeliunxp2f  8265  tpostpos  8301  ecdmn0  8808  brecop2  8870  elixpsn  9003  bren  9021  0sdom1dom  9275  elharval  9592  brttrcl  9751  sdom2en01  10419  isfin1-2  10502  wdomac  10645  elwina  10810  elina  10811  lterpq  11094  ltrnq  11103  elnp  11111  elnpi  11112  ltresr  11264  eluz2  13011  dfle2  13316  dflt2  13317  rexanuz2  15561  even2n  16556  isstruct2  17371  xpsfrnel2  17786  ismre  17810  isacs  17875  brssc  18039  isfunc  18089  oduclatb  18731  isipodrs  18761  issubg  19386  isnsg  19415  oppgsubm  19627  oppgsubg  19628  isslw  19873  efgrelexlema  20014  dvdsr  20643  isunit  20654  isirred  20700  isrim0  20764  issubrng  20850  opprsubrng  20862  issubrg  20874  opprsubrg  20896  islss  21260  islbs4  22193  istopon  23285  basdif0  23326  dis2ndc  23834  elmptrab  24201  isusp  24635  ismet2  24707  isphtpc  25370  elpi1  25421  iscmet  25660  bcthlem1  25700  elno  28060  elz12s  28915  dfz12s2  28931  wlkcpr  30266  isvcOLD  31238  isnv  31271  hlimi  31847  h1de2ci  32215  elunop  32531  ispcmp  34600  elmpps  36546  eldm3  36741  opelco3  36754  elima4  36755  brsset  36866  brbigcup  36875  elfix2  36881  elsingles  36895  imageval  36907  funpartlem  36921  elaltxp  36955  ellines  37132  isfne4  37343  bj-ismoore  38296  bj-idreseqb  38352  istotbnd  38969  isbnd  38980  isdrngo1  39156  isnacs  43981  sbccomieg  44066  elmnc  44403  ismea  47734  isinv2  50471  oppcinito  50688  oppctermo  50689  oppczeroo  50690  catcsect  50864  lmdfval2  51169  cmdfval2  51170  initocmd  51183  termolmd  51184