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  2880  elrabf  3680  elrab  3684  sbccow  3801  sbcco  3804  sbc5ALT  3807  sbcan  3830  sbcor  3831  sbcal  3842  sbcex2  3843  sbcel1v  3849  sbcreu  3871  eldif  3959  elin  3965  elun  4149  sbccsb2  4435  2reu4  4527  elpr2OLD  4655  eluni  4912  eliun  5002  sbcbr123  5203  elopab  5528  opelopabsb  5531  opeliunxp2  5839  inisegn0  6098  brfvopabrbr  6996  elpwun  7756  elxp5  7914  opeliunxp2f  8195  tpostpos  8231  ecdmn0  8750  brecop2  8805  elixpsn  8931  bren  8949  brenOLD  8950  0sdom1dom  9238  elharval  9556  brttrcl  9708  sdom2en01  10297  isfin1-2  10380  wdomac  10522  elwina  10681  elina  10682  lterpq  10965  ltrnq  10974  elnp  10982  elnpi  10983  ltresr  11135  eluz2  12828  dfle2  13126  dflt2  13127  rexanuz2  15296  even2n  16285  isstruct2  17082  xpsfrnel2  17510  ismre  17534  isacs  17595  brssc  17761  isfunc  17814  oduclatb  18460  isipodrs  18490  issubg  19006  isnsg  19035  oppgsubm  19229  oppgsubg  19230  isslw  19476  efgrelexlema  19617  dvdsr  20176  isunit  20187  isirred  20233  isrim0  20261  issubrg  20319  opprsubrg  20340  islss  20545  islbs4  21387  istopon  22414  basdif0  22456  dis2ndc  22964  elmptrab  23331  isusp  23766  ismet2  23839  isphtpc  24510  elpi1  24561  iscmet  24801  bcthlem1  24841  elno  27149  wlkcpr  28886  isvcOLD  29832  isnv  29865  hlimi  30441  h1de2ci  30809  elunop  31125  ispcmp  32837  elmpps  34564  eldm3  34731  opelco3  34746  elima4  34747  brsset  34861  brbigcup  34870  elfix2  34876  elsingles  34890  imageval  34902  funpartlem  34914  elaltxp  34947  ellines  35124  isfne4  35225  bj-ismoore  35986  bj-idreseqb  36044  istotbnd  36637  isbnd  36648  isdrngo1  36824  elrab2w  41410  isnacs  41442  sbccomieg  41531  elmnc  41878  ismea  45167  issubrng  46726  opprsubrng  46738