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  3234  exmidn0m  4235  euotd  4288  ralxfr2d  4500  rexxfr2d  4501  nlimsucg  4603  wetriext  4614  relop  4817  resiexg  4992  iotass  5237  fnbr  5363  f1o00  5542  foelcdmi  5616  fnex  5787  foelrn  5802  acexmidlemab  5919  f1ocnv2d  6131  ofrval  6150  eloprabi  6263  1stconst  6288  2ndconst  6289  poxp  6299  smodm2  6362  smoiso  6369  nnsucuniel  6562  erth  6647  iinerm  6675  pw2f1odclem  6904  pw2f1odc  6905  phplem4dom  6932  findcard2  6959  findcard2s  6960  fimax2gtrilemstep  6970  undifdcss  6993  tpfidceq  7000  fipwssg  7054  supelti  7077  nlt1pig  7425  dfplpq2  7438  ltsonq  7482  archnqq  7501  nqnq0pi  7522  prarloclemn  7583  genprndl  7605  genprndu  7606  genpdisj  7607  addlocprlemgt  7618  addlocpr  7620  nqprl  7635  nqpru  7636  addnqprlemrl  7641  addnqprlemru  7642  mulnqprlemrl  7657  mulnqprlemru  7658  ltpopr  7679  ltexprlemloc  7691  ltexprlemrl  7694  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  caucvgprlemladdfu  7761  suplocexprlemru  7803  axcaucvglemres  7983  cnegex  8221  mullt0  8524  eqord1  8527  mulge0  8663  divap0  8728  div2negap  8779  prodgt0  8896  ltmul12a  8904  recgt1i  8942  div4p1lem1div2  9262  nn0lt2  9424  peano5uzti  9451  btwnapz  9473  eluzp1m1  9642  eluzaddi  9645  eluzsubi  9646  uz2m1nn  9696  rphalflt  9775  xleaddadd  9979  ixxdisj  9995  iccgelb  10024  icodisj  10084  iccf1o  10096  fzsuc2  10171  fzonmapblen  10280  zsupcllemstep  10336  nninfdcex  10344  flqge0nn0  10400  flqge1nn  10401  modfzo0difsn  10504  nninfinf  10552  seqf1oglem2  10629  expubnd  10705  bernneq  10769  bernneq2  10770  nn0opthlem2d  10830  facwordi  10849  bcpasc  10875  hashnncl  10904  recvguniq  11177  sqrt0rlem  11185  resqrexlemover  11192  resqrexlemcalc3  11198  resqrexlemgt0  11202  resqrexlemoverl  11203  recvalap  11279  nnabscl  11282  negfi  11410  2zinfmin  11425  climi0  11471  climge0  11507  summodclem3  11562  fsumsplit  11589  fisumcom2  11620  fisumrev2  11628  explecnv  11687  cvgratnnlemseq  11708  fprodsplitdc  11778  fprodsplit  11779  fprodcom2fi  11808  eftlub  11872  sin02gt0  11946  dvdslelemd  12025  dvdsleabs2  12028  mulmoddvds  12045  odd2np1  12055  oexpneg  12059  mod2eq1n2dvds  12061  sqoddm1div8z  12068  rplpwr  12219  rppwr  12220  nn0seqcvgd  12234  lcmneg  12267  qredeq  12289  dvdsnprmd  12318  oddprmge3  12328  oddpwdclemdvds  12363  oddpwdclemndvds  12364  oddpwdclemodd  12365  znege1  12371  qgt0numnn  12392  phibndlem  12409  hashgcdeq  12433  reumodprminv  12447  coprimeprodsq2  12452  pythagtrip  12477  pceq0  12516  dvdsprmpweqle  12531  fldivp1  12542  4sqlem9  12580  4sqlem15  12599  4sqlem16  12600  ennnfonelemf1  12660  imasmnd  13155  imasgrp  13317  subginv  13387  subgmulg  13394  eqger  13430  kerf1ghm  13480  rngpropd  13587  srgidmlem  13610  srg1zr  13619  ringpropd  13670  crngpropd  13671  imasring  13696  rhmf1o  13800  subrngpropd  13848  subrg1  13863  subrgpropd  13885  rrgnz  13900  aprsym  13916  aprcotr  13917  lmodprop2d  13980  lssssg  13992  lss0cl  14001  isridlrng  14114  rspcl  14123  rspssid  14124  rnglidlmmgm  14128  psrgrp  14313  neiuni  14481  neissex  14485  tgrest  14489  tgcnp  14529  lmfpm  14563  lmcl  14565  lmss  14566  lmff  14569  psmetdmdm  14644  xmeter  14756  neibl  14811  xmettxlem  14829  tgqioo  14875  cnopnap  14931  limcimo  14985  dvidsslem  15013  sinq12gt0  15150  logrpap0  15197  mersenne  15317  lgsdilem  15352  lgsdinn0  15373  gausslemma2dlem0b  15375  gausslemma2dlem1a  15383  gausslemma2dlem5  15391  gausslemma2dlem6  15392  lgsquad3  15409  m1lgs  15410  2lgslem1a  15413  2lgslem1  15416  2lgslem3a1  15422  2lgslem3b1  15423  2lgslem3c1  15424  2lgslem3d1  15425  2sqlem6  15445  2omap  15726  isomninnlem  15761  ismkvnnlem  15783