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  2772  cgsex2g  2773  cgsex4g  2774  ceqsex  2775  sbciegft  2993  sbeqalb  3019  sseqtrid  3205  exmidn0m  4199  euotd  4252  ralxfr2d  4462  rexxfr2d  4463  nlimsucg  4563  wetriext  4574  relop  4774  resiexg  4949  iotass  5192  fnbr  5315  f1o00  5493  foelcdmi  5565  fnex  5735  foelrn  5749  acexmidlemab  5864  f1ocnv2d  6070  ofrval  6088  eloprabi  6192  1stconst  6217  2ndconst  6218  poxp  6228  smodm2  6291  smoiso  6298  nnsucuniel  6491  erth  6574  iinerm  6602  phplem4dom  6857  findcard2  6884  findcard2s  6885  fimax2gtrilemstep  6895  undifdcss  6917  fipwssg  6973  supelti  6996  nlt1pig  7335  dfplpq2  7348  ltsonq  7392  archnqq  7411  nqnq0pi  7432  prarloclemn  7493  genprndl  7515  genprndu  7516  genpdisj  7517  addlocprlemgt  7528  addlocpr  7530  nqprl  7545  nqpru  7546  addnqprlemrl  7551  addnqprlemru  7552  mulnqprlemrl  7567  mulnqprlemru  7568  ltpopr  7589  ltexprlemloc  7601  ltexprlemrl  7604  cauappcvgprlemladdfu  7648  cauappcvgprlemladdfl  7649  caucvgprlemladdfu  7671  suplocexprlemru  7713  axcaucvglemres  7893  cnegex  8129  mullt0  8431  eqord1  8434  mulge0  8570  divap0  8635  div2negap  8686  prodgt0  8803  ltmul12a  8811  recgt1i  8849  div4p1lem1div2  9166  nn0lt2  9328  peano5uzti  9355  btwnapz  9377  eluzp1m1  9545  eluzaddi  9548  eluzsubi  9549  uz2m1nn  9599  rphalflt  9677  xleaddadd  9881  ixxdisj  9897  iccgelb  9926  icodisj  9986  iccf1o  9998  fzsuc2  10072  fzonmapblen  10180  flqge0nn0  10286  flqge1nn  10287  modfzo0difsn  10388  expubnd  10570  bernneq  10633  bernneq2  10634  nn0opthlem2d  10692  facwordi  10711  bcpasc  10737  hashnncl  10766  recvguniq  10995  sqrt0rlem  11003  resqrexlemover  11010  resqrexlemcalc3  11016  resqrexlemgt0  11020  resqrexlemoverl  11021  recvalap  11097  nnabscl  11100  negfi  11227  2zinfmin  11242  climi0  11288  climge0  11324  summodclem3  11379  fsumsplit  11406  fisumcom2  11437  fisumrev2  11445  explecnv  11504  cvgratnnlemseq  11525  fprodsplitdc  11595  fprodsplit  11596  fprodcom2fi  11625  eftlub  11689  sin02gt0  11762  dvdslelemd  11839  dvdsleabs2  11842  mulmoddvds  11859  odd2np1  11868  oexpneg  11872  mod2eq1n2dvds  11874  sqoddm1div8z  11881  zsupcllemstep  11936  nninfdcex  11944  rplpwr  12018  rppwr  12019  nn0seqcvgd  12031  lcmneg  12064  qredeq  12086  dvdsnprmd  12115  oddprmge3  12125  oddpwdclemdvds  12160  oddpwdclemndvds  12161  oddpwdclemodd  12162  znege1  12168  qgt0numnn  12189  phibndlem  12206  hashgcdeq  12229  reumodprminv  12243  coprimeprodsq2  12248  pythagtrip  12273  pceq0  12311  dvdsprmpweqle  12326  fldivp1  12336  4sqlem9  12374  ennnfonelemf1  12409  subginv  12967  subgmulg  12974  srgidmlem  13061  srg1zr  13070  ringpropd  13117  crngpropd  13118  aprsym  13241  aprcotr  13242  neiuni  13443  neissex  13447  tgrest  13451  tgcnp  13491  lmfpm  13525  lmcl  13527  lmss  13528  lmff  13531  psmetdmdm  13606  xmeter  13718  neibl  13773  xmettxlem  13791  tgqioo  13829  cnopnap  13876  limcimo  13916  sinq12gt0  14033  logrpap0  14080  lgsdilem  14210  lgsdinn0  14231  2sqlem6  14238  isomninnlem  14549  ismkvnnlem  14571