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  605  biadanid  618  bimsc1  971  biimp3a  1381  equsex  1776  euor  2105  euan  2136  cgsexg  2838  cgsex2g  2839  cgsex4g  2840  ceqsex  2841  sbciegft  3062  sbeqalb  3088  sseqtrid  3277  exmidn0m  4291  euotd  4347  ralxfr2d  4561  rexxfr2d  4562  nlimsucg  4664  wetriext  4675  relop  4880  resiexg  5058  iotass  5304  fnbr  5434  f1o00  5620  foelcdmi  5698  fnex  5875  foelrn  5892  riotaeqimp  5995  acexmidlemab  6011  f1ocnv2d  6226  ofrval  6245  eloprabi  6360  1stconst  6385  2ndconst  6386  poxp  6396  smodm2  6460  smoiso  6467  nnsucuniel  6662  erth  6747  iinerm  6775  pw2f1odclem  7019  pw2f1odc  7020  phplem4dom  7047  findcard2  7077  findcard2s  7078  fimax2gtrilemstep  7089  undifdcss  7114  tpfidceq  7121  fipwssg  7177  supelti  7200  nlt1pig  7560  dfplpq2  7573  ltsonq  7617  archnqq  7636  nqnq0pi  7657  prarloclemn  7718  genprndl  7740  genprndu  7741  genpdisj  7742  addlocprlemgt  7753  addlocpr  7755  nqprl  7770  nqpru  7771  addnqprlemrl  7776  addnqprlemru  7777  mulnqprlemrl  7792  mulnqprlemru  7793  ltpopr  7814  ltexprlemloc  7826  ltexprlemrl  7829  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  caucvgprlemladdfu  7896  suplocexprlemru  7938  axcaucvglemres  8118  cnegex  8356  mullt0  8659  eqord1  8662  mulge0  8798  divap0  8863  div2negap  8914  prodgt0  9031  ltmul12a  9039  recgt1i  9077  div4p1lem1div2  9397  nn0lt2  9560  peano5uzti  9587  btwnapz  9609  eluzp1m1  9779  eluzaddi  9782  eluzsubi  9783  uz2m1nn  9838  rphalflt  9917  xleaddadd  10121  ixxdisj  10137  iccgelb  10166  icodisj  10226  iccf1o  10238  fzsuc2  10313  fzonmapblen  10425  zsupcllemstep  10488  nninfdcex  10496  flqge0nn0  10552  flqge1nn  10553  modfzo0difsn  10656  nninfinf  10704  seqf1oglem2  10781  expubnd  10857  bernneq  10921  bernneq2  10922  nn0opthlem2d  10982  facwordi  11001  bcpasc  11027  hashnncl  11056  ccatsymb  11178  ccatass  11184  ccat1st1st  11217  fzowrddc  11227  swrdlend  11238  swrdfv2  11243  swrdspsleq  11247  pfxeq  11276  pfxsuff1eqwrdeq  11279  swrdswrdlem  11284  swrdswrd  11285  swrdpfx  11287  ccats1pfxeqrex  11295  pfxccatin12lem1  11308  swrdccatin2  11309  recvguniq  11555  sqrt0rlem  11563  resqrexlemover  11570  resqrexlemcalc3  11576  resqrexlemgt0  11580  resqrexlemoverl  11581  recvalap  11657  nnabscl  11660  negfi  11788  2zinfmin  11803  climi0  11849  climge0  11885  summodclem3  11940  fsumsplit  11967  fisumcom2  11998  fisumrev2  12006  explecnv  12065  cvgratnnlemseq  12086  fprodsplitdc  12156  fprodsplit  12157  fprodcom2fi  12186  eftlub  12250  sin02gt0  12324  dvdslelemd  12403  dvdsleabs2  12406  mulmoddvds  12423  odd2np1  12433  oexpneg  12437  mod2eq1n2dvds  12439  sqoddm1div8z  12446  rplpwr  12597  rppwr  12598  nn0seqcvgd  12612  lcmneg  12645  qredeq  12667  dvdsnprmd  12696  oddprmge3  12706  oddpwdclemdvds  12741  oddpwdclemndvds  12742  oddpwdclemodd  12743  znege1  12749  qgt0numnn  12770  phibndlem  12787  hashgcdeq  12811  reumodprminv  12825  coprimeprodsq2  12830  pythagtrip  12855  pceq0  12894  dvdsprmpweqle  12909  fldivp1  12920  4sqlem9  12958  4sqlem15  12977  4sqlem16  12978  ennnfonelemf1  13038  imasmnd  13535  imasgrp  13697  subginv  13767  subgmulg  13774  eqger  13810  kerf1ghm  13860  rngpropd  13967  srgidmlem  13990  srg1zr  13999  ringpropd  14050  crngpropd  14051  imasring  14076  rhmf1o  14181  subrngpropd  14229  subrg1  14244  subrgpropd  14266  rrgnz  14281  aprsym  14297  aprcotr  14298  lmodprop2d  14361  lssssg  14373  lss0cl  14382  isridlrng  14495  rspcl  14504  rspssid  14505  rnglidlmmgm  14509  psrgrp  14698  mplsubgfilemcl  14712  neiuni  14884  neissex  14888  tgrest  14892  tgcnp  14932  lmfpm  14966  lmcl  14968  lmss  14969  lmff  14972  psmetdmdm  15047  xmeter  15159  neibl  15214  xmettxlem  15232  tgqioo  15278  cnopnap  15334  limcimo  15388  dvidsslem  15416  sinq12gt0  15553  logrpap0  15600  mersenne  15720  lgsdilem  15755  lgsdinn0  15776  gausslemma2dlem0b  15778  gausslemma2dlem1a  15786  gausslemma2dlem5  15794  gausslemma2dlem6  15795  lgsquad3  15812  m1lgs  15813  2lgslem1a  15816  2lgslem1  15819  2lgslem3a1  15825  2lgslem3b1  15826  2lgslem3c1  15827  2lgslem3d1  15828  2sqlem6  15848  edgupgren  15991  upgredg  15994  wlkl1loop  16208  wlk1walkdom  16209  upgriswlkdc  16210  loopclwwlkn1b  16269  2omap  16594  isomninnlem  16634  ismkvnnlem  16656