Theorem biimpa 296

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 144	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	imp 124	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  simprbda  383  simplbda  384  pm5.1  601  bimsc1  963  biimp3a  1345  equsex  1728  euor  2052  euan  2082  cgsexg  2773  cgsex2g  2774  cgsex4g  2775  ceqsex  2776  sbciegft  2994  sbeqalb  3020  sseqtrid  3206  exmidn0m  4202  euotd  4255  ralxfr2d  4465  rexxfr2d  4466  nlimsucg  4566  wetriext  4577  relop  4778  resiexg  4953  iotass  5196  fnbr  5319  f1o00  5497  foelcdmi  5569  fnex  5739  foelrn  5754  acexmidlemab  5869  f1ocnv2d  6075  ofrval  6093  eloprabi  6197  1stconst  6222  2ndconst  6223  poxp  6233  smodm2  6296  smoiso  6303  nnsucuniel  6496  erth  6579  iinerm  6607  phplem4dom  6862  findcard2  6889  findcard2s  6890  fimax2gtrilemstep  6900  undifdcss  6922  fipwssg  6978  supelti  7001  nlt1pig  7340  dfplpq2  7353  ltsonq  7397  archnqq  7416  nqnq0pi  7437  prarloclemn  7498  genprndl  7520  genprndu  7521  genpdisj  7522  addlocprlemgt  7533  addlocpr  7535  nqprl  7550  nqpru  7551  addnqprlemrl  7556  addnqprlemru  7557  mulnqprlemrl  7572  mulnqprlemru  7573  ltpopr  7594  ltexprlemloc  7606  ltexprlemrl  7609  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  caucvgprlemladdfu  7676  suplocexprlemru  7718  axcaucvglemres  7898  cnegex  8135  mullt0  8437  eqord1  8440  mulge0  8576  divap0  8641  div2negap  8692  prodgt0  8809  ltmul12a  8817  recgt1i  8855  div4p1lem1div2  9172  nn0lt2  9334  peano5uzti  9361  btwnapz  9383  eluzp1m1  9551  eluzaddi  9554  eluzsubi  9555  uz2m1nn  9605  rphalflt  9683  xleaddadd  9887  ixxdisj  9903  iccgelb  9932  icodisj  9992  iccf1o  10004  fzsuc2  10079  fzonmapblen  10187  flqge0nn0  10293  flqge1nn  10294  modfzo0difsn  10395  expubnd  10577  bernneq  10641  bernneq2  10642  nn0opthlem2d  10701  facwordi  10720  bcpasc  10746  hashnncl  10775  recvguniq  11004  sqrt0rlem  11012  resqrexlemover  11019  resqrexlemcalc3  11025  resqrexlemgt0  11029  resqrexlemoverl  11030  recvalap  11106  nnabscl  11109  negfi  11236  2zinfmin  11251  climi0  11297  climge0  11333  summodclem3  11388  fsumsplit  11415  fisumcom2  11446  fisumrev2  11454  explecnv  11513  cvgratnnlemseq  11534  fprodsplitdc  11604  fprodsplit  11605  fprodcom2fi  11634  eftlub  11698  sin02gt0  11771  dvdslelemd  11849  dvdsleabs2  11852  mulmoddvds  11869  odd2np1  11878  oexpneg  11882  mod2eq1n2dvds  11884  sqoddm1div8z  11891  zsupcllemstep  11946  nninfdcex  11954  rplpwr  12028  rppwr  12029  nn0seqcvgd  12041  lcmneg  12074  qredeq  12096  dvdsnprmd  12125  oddprmge3  12135  oddpwdclemdvds  12170  oddpwdclemndvds  12171  oddpwdclemodd  12172  znege1  12178  qgt0numnn  12199  phibndlem  12216  hashgcdeq  12239  reumodprminv  12253  coprimeprodsq2  12258  pythagtrip  12283  pceq0  12321  dvdsprmpweqle  12336  fldivp1  12346  4sqlem9  12384  ennnfonelemf1  12419  subginv  13041  subgmulg  13048  eqger  13083  srgidmlem  13161  srg1zr  13170  ringpropd  13217  crngpropd  13218  subrg1  13352  subrgpropd  13369  aprsym  13374  aprcotr  13375  lmodprop2d  13438  neiuni  13664  neissex  13668  tgrest  13672  tgcnp  13712  lmfpm  13746  lmcl  13748  lmss  13749  lmff  13752  psmetdmdm  13827  xmeter  13939  neibl  13994  xmettxlem  14012  tgqioo  14050  cnopnap  14097  limcimo  14137  sinq12gt0  14254  logrpap0  14301  lgsdilem  14431  lgsdinn0  14452  m1lgs  14455  2sqlem6  14470  isomninnlem  14781  ismkvnnlem  14803