Theorem biimpa 291

Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)

Hypothesis

Ref	Expression
biimpa.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpa	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem biimpa

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpd 143	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	imp 123	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  simprbda  376  simplbda  377  pm5.1  569  bimsc1  912  biimp3a  1288  equsex  1670  euor  1981  euan  2011  cgsexg  2668  cgsex2g  2669  cgsex4g  2670  ceqsex  2671  sbciegft  2883  sbeqalb  2909  syl5sseq  3089  exmidn0m  4054  euotd  4105  ralxfr2d  4314  rexxfr2d  4315  nlimsucg  4410  wetriext  4420  relop  4617  resiexg  4790  iotass  5031  fnbr  5150  f1o00  5323  fnex  5558  foelrn  5570  acexmidlemab  5684  f1ocnv2d  5886  ofrval  5904  eloprabi  6004  1stconst  6024  2ndconst  6025  poxp  6035  smodm2  6098  smoiso  6105  nnsucuniel  6296  erth  6376  iinerm  6404  phplem4dom  6658  findcard2  6685  findcard2s  6686  fimax2gtrilemstep  6696  undifdcss  6713  supelti  6777  nlt1pig  6997  dfplpq2  7010  ltsonq  7054  archnqq  7073  nqnq0pi  7094  prarloclemn  7155  genprndl  7177  genprndu  7178  genpdisj  7179  addlocprlemgt  7190  addlocpr  7192  nqprl  7207  nqpru  7208  addnqprlemrl  7213  addnqprlemru  7214  mulnqprlemrl  7229  mulnqprlemru  7230  ltpopr  7251  ltexprlemloc  7263  ltexprlemrl  7266  cauappcvgprlemladdfu  7310  cauappcvgprlemladdfl  7311  caucvgprlemladdfu  7333  axcaucvglemres  7531  cnegex  7757  mullt0  8055  eqord1  8058  mulge0  8193  divap0  8248  div2negap  8299  prodgt0  8410  ltmul12a  8418  recgt1i  8456  div4p1lem1div2  8767  nn0lt2  8926  peano5uzti  8953  btwnapz  8975  eluzp1m1  9141  eluzaddi  9144  eluzsubi  9145  uz2m1nn  9191  rphalflt  9262  xleaddadd  9453  ixxdisj  9469  iccgelb  9498  icodisj  9558  iccf1o  9570  fzsuc2  9642  fzonmapblen  9747  flqge0nn0  9849  flqge1nn  9850  modfzo0difsn  9951  expubnd  10143  bernneq  10205  bernneq2  10206  nn0opthlem2d  10260  facwordi  10279  bcpasc  10305  hashnncl  10335  recvguniq  10559  sqrt0rlem  10567  resqrexlemover  10574  resqrexlemcalc3  10580  resqrexlemgt0  10584  resqrexlemoverl  10585  recvalap  10661  nnabscl  10664  negfi  10790  climi0  10848  climge0  10884  summodclem3  10939  fsumsplit  10966  fisumcom2  10997  fisumrev2  11005  explecnv  11064  cvgratnnlemseq  11085  eftlub  11145  sin02gt0  11219  dvdslelemd  11287  dvdsleabs2  11290  mulmoddvds  11307  odd2np1  11316  oexpneg  11320  mod2eq1n2dvds  11322  sqoddm1div8z  11329  zsupcllemstep  11384  rplpwr  11459  rppwr  11460  nn0seqcvgd  11466  lcmneg  11499  qredeq  11521  dvdsnprmd  11550  oddprmge3  11559  oddpwdclemdvds  11591  oddpwdclemndvds  11592  oddpwdclemodd  11593  znege1  11599  qgt0numnn  11620  phibndlem  11635  hashgcdeq  11647  neiuni  12029  neissex  12033  tgrest  12037  tgcnp  12076  lmfpm  12110  lmcl  12112  lmss  12113  lmff  12116  psmetdmdm  12126  xmeter  12238  neibl  12293  tgqioo  12337