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  1742  euor  2071  euan  2101  cgsexg  2798  cgsex2g  2799  cgsex4g  2800  ceqsex  2801  sbciegft  3020  sbeqalb  3046  sseqtrid  3233  exmidn0m  4234  euotd  4287  ralxfr2d  4499  rexxfr2d  4500  nlimsucg  4602  wetriext  4613  relop  4816  resiexg  4991  iotass  5236  fnbr  5360  f1o00  5539  foelcdmi  5613  fnex  5784  foelrn  5799  acexmidlemab  5916  f1ocnv2d  6127  ofrval  6146  eloprabi  6254  1stconst  6279  2ndconst  6280  poxp  6290  smodm2  6353  smoiso  6360  nnsucuniel  6553  erth  6638  iinerm  6666  pw2f1odclem  6895  pw2f1odc  6896  phplem4dom  6923  findcard2  6950  findcard2s  6951  fimax2gtrilemstep  6961  undifdcss  6984  tpfidceq  6991  fipwssg  7045  supelti  7068  nlt1pig  7408  dfplpq2  7421  ltsonq  7465  archnqq  7484  nqnq0pi  7505  prarloclemn  7566  genprndl  7588  genprndu  7589  genpdisj  7590  addlocprlemgt  7601  addlocpr  7603  nqprl  7618  nqpru  7619  addnqprlemrl  7624  addnqprlemru  7625  mulnqprlemrl  7640  mulnqprlemru  7641  ltpopr  7662  ltexprlemloc  7674  ltexprlemrl  7677  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  caucvgprlemladdfu  7744  suplocexprlemru  7786  axcaucvglemres  7966  cnegex  8204  mullt0  8507  eqord1  8510  mulge0  8646  divap0  8711  div2negap  8762  prodgt0  8879  ltmul12a  8887  recgt1i  8925  div4p1lem1div2  9245  nn0lt2  9407  peano5uzti  9434  btwnapz  9456  eluzp1m1  9625  eluzaddi  9628  eluzsubi  9629  uz2m1nn  9679  rphalflt  9758  xleaddadd  9962  ixxdisj  9978  iccgelb  10007  icodisj  10067  iccf1o  10079  fzsuc2  10154  fzonmapblen  10263  zsupcllemstep  10319  nninfdcex  10327  flqge0nn0  10383  flqge1nn  10384  modfzo0difsn  10487  nninfinf  10535  seqf1oglem2  10612  expubnd  10688  bernneq  10752  bernneq2  10753  nn0opthlem2d  10813  facwordi  10832  bcpasc  10858  hashnncl  10887  recvguniq  11160  sqrt0rlem  11168  resqrexlemover  11175  resqrexlemcalc3  11181  resqrexlemgt0  11185  resqrexlemoverl  11186  recvalap  11262  nnabscl  11265  negfi  11393  2zinfmin  11408  climi0  11454  climge0  11490  summodclem3  11545  fsumsplit  11572  fisumcom2  11603  fisumrev2  11611  explecnv  11670  cvgratnnlemseq  11691  fprodsplitdc  11761  fprodsplit  11762  fprodcom2fi  11791  eftlub  11855  sin02gt0  11929  dvdslelemd  12008  dvdsleabs2  12011  mulmoddvds  12028  odd2np1  12038  oexpneg  12042  mod2eq1n2dvds  12044  sqoddm1div8z  12051  rplpwr  12194  rppwr  12195  nn0seqcvgd  12209  lcmneg  12242  qredeq  12264  dvdsnprmd  12293  oddprmge3  12303  oddpwdclemdvds  12338  oddpwdclemndvds  12339  oddpwdclemodd  12340  znege1  12346  qgt0numnn  12367  phibndlem  12384  hashgcdeq  12408  reumodprminv  12422  coprimeprodsq2  12427  pythagtrip  12452  pceq0  12491  dvdsprmpweqle  12506  fldivp1  12517  4sqlem9  12555  4sqlem15  12574  4sqlem16  12575  ennnfonelemf1  12635  imasgrp  13241  subginv  13311  subgmulg  13318  eqger  13354  kerf1ghm  13404  rngpropd  13511  srgidmlem  13534  srg1zr  13543  ringpropd  13594  crngpropd  13595  imasring  13620  rhmf1o  13724  subrngpropd  13772  subrg1  13787  subrgpropd  13809  rrgnz  13824  aprsym  13840  aprcotr  13841  lmodprop2d  13904  lssssg  13916  lss0cl  13925  isridlrng  14038  rspcl  14047  rspssid  14048  rnglidlmmgm  14052  neiuni  14397  neissex  14401  tgrest  14405  tgcnp  14445  lmfpm  14479  lmcl  14481  lmss  14482  lmff  14485  psmetdmdm  14560  xmeter  14672  neibl  14727  xmettxlem  14745  tgqioo  14791  cnopnap  14847  limcimo  14901  dvidsslem  14929  sinq12gt0  15066  logrpap0  15113  mersenne  15233  lgsdilem  15268  lgsdinn0  15289  gausslemma2dlem0b  15291  gausslemma2dlem1a  15299  gausslemma2dlem5  15307  gausslemma2dlem6  15308  lgsquad3  15325  m1lgs  15326  2lgslem1a  15329  2lgslem1  15332  2lgslem3a1  15338  2lgslem3b1  15339  2lgslem3c1  15340  2lgslem3d1  15341  2sqlem6  15361  isomninnlem  15674  ismkvnnlem  15696