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  biadanid  614  bimsc1  965  biimp3a  1356  equsex  1739  euor  2068  euan  2098  cgsexg  2795  cgsex2g  2796  cgsex4g  2797  ceqsex  2798  sbciegft  3016  sbeqalb  3042  sseqtrid  3229  exmidn0m  4230  euotd  4283  ralxfr2d  4495  rexxfr2d  4496  nlimsucg  4598  wetriext  4609  relop  4812  resiexg  4987  iotass  5232  fnbr  5356  f1o00  5535  foelcdmi  5609  fnex  5780  foelrn  5795  acexmidlemab  5912  f1ocnv2d  6122  ofrval  6141  eloprabi  6249  1stconst  6274  2ndconst  6275  poxp  6285  smodm2  6348  smoiso  6355  nnsucuniel  6548  erth  6633  iinerm  6661  pw2f1odclem  6890  pw2f1odc  6891  phplem4dom  6918  findcard2  6945  findcard2s  6946  fimax2gtrilemstep  6956  undifdcss  6979  fipwssg  7038  supelti  7061  nlt1pig  7401  dfplpq2  7414  ltsonq  7458  archnqq  7477  nqnq0pi  7498  prarloclemn  7559  genprndl  7581  genprndu  7582  genpdisj  7583  addlocprlemgt  7594  addlocpr  7596  nqprl  7611  nqpru  7612  addnqprlemrl  7617  addnqprlemru  7618  mulnqprlemrl  7633  mulnqprlemru  7634  ltpopr  7655  ltexprlemloc  7667  ltexprlemrl  7670  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  caucvgprlemladdfu  7737  suplocexprlemru  7779  axcaucvglemres  7959  cnegex  8197  mullt0  8499  eqord1  8502  mulge0  8638  divap0  8703  div2negap  8754  prodgt0  8871  ltmul12a  8879  recgt1i  8917  div4p1lem1div2  9236  nn0lt2  9398  peano5uzti  9425  btwnapz  9447  eluzp1m1  9616  eluzaddi  9619  eluzsubi  9620  uz2m1nn  9670  rphalflt  9749  xleaddadd  9953  ixxdisj  9969  iccgelb  9998  icodisj  10058  iccf1o  10070  fzsuc2  10145  fzonmapblen  10254  flqge0nn0  10362  flqge1nn  10363  modfzo0difsn  10466  nninfinf  10514  seqf1oglem2  10591  expubnd  10667  bernneq  10731  bernneq2  10732  nn0opthlem2d  10792  facwordi  10811  bcpasc  10837  hashnncl  10866  recvguniq  11139  sqrt0rlem  11147  resqrexlemover  11154  resqrexlemcalc3  11160  resqrexlemgt0  11164  resqrexlemoverl  11165  recvalap  11241  nnabscl  11244  negfi  11371  2zinfmin  11386  climi0  11432  climge0  11468  summodclem3  11523  fsumsplit  11550  fisumcom2  11581  fisumrev2  11589  explecnv  11648  cvgratnnlemseq  11669  fprodsplitdc  11739  fprodsplit  11740  fprodcom2fi  11769  eftlub  11833  sin02gt0  11907  dvdslelemd  11985  dvdsleabs2  11988  mulmoddvds  12005  odd2np1  12014  oexpneg  12018  mod2eq1n2dvds  12020  sqoddm1div8z  12027  zsupcllemstep  12082  nninfdcex  12090  rplpwr  12164  rppwr  12165  nn0seqcvgd  12179  lcmneg  12212  qredeq  12234  dvdsnprmd  12263  oddprmge3  12273  oddpwdclemdvds  12308  oddpwdclemndvds  12309  oddpwdclemodd  12310  znege1  12316  qgt0numnn  12337  phibndlem  12354  hashgcdeq  12377  reumodprminv  12391  coprimeprodsq2  12396  pythagtrip  12421  pceq0  12460  dvdsprmpweqle  12475  fldivp1  12486  4sqlem9  12524  4sqlem15  12543  4sqlem16  12544  ennnfonelemf1  12575  imasgrp  13181  subginv  13251  subgmulg  13258  eqger  13294  kerf1ghm  13344  rngpropd  13451  srgidmlem  13474  srg1zr  13483  ringpropd  13534  crngpropd  13535  imasring  13560  rhmf1o  13664  subrngpropd  13712  subrg1  13727  subrgpropd  13749  rrgnz  13764  aprsym  13780  aprcotr  13781  lmodprop2d  13844  lssssg  13856  lss0cl  13865  isridlrng  13978  rspcl  13987  rspssid  13988  rnglidlmmgm  13992  neiuni  14329  neissex  14333  tgrest  14337  tgcnp  14377  lmfpm  14411  lmcl  14413  lmss  14414  lmff  14417  psmetdmdm  14492  xmeter  14604  neibl  14659  xmettxlem  14677  tgqioo  14715  cnopnap  14765  limcimo  14819  sinq12gt0  14965  logrpap0  15012  lgsdilem  15143  lgsdinn0  15164  gausslemma2dlem0b  15166  gausslemma2dlem1a  15174  gausslemma2dlem5  15182  gausslemma2dlem6  15183  m1lgs  15192  2sqlem6  15207  isomninnlem  15520  ismkvnnlem  15542