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  972  biimp3a  1382  equsex  1776  euor  2108  euan  2139  cgsexg  2851  cgsex2g  2852  cgsex4g  2853  ceqsex  2854  sbciegft  3076  sbeqalb  3102  sseqtrid  3292  exmidn0m  4319  euotd  4376  ralxfr2d  4590  rexxfr2d  4591  nlimsucg  4693  wetriext  4704  relop  4910  resiexg  5088  iotass  5335  fnbr  5465  f1o00  5656  foelcdmi  5734  fnex  5911  foelrn  5931  riotaeqimp  6036  acexmidlemab  6052  f1ocnv2d  6267  f1o3d  6271  ofrval  6286  elabreximd  6329  eloprabi  6405  1stconst  6430  2ndconst  6431  poxp  6441  smodm2  6539  smoiso  6546  nnsucuniel  6741  erth  6826  iinerm  6854  pw2f1odclem  7100  pw2f1odc  7101  phplem4dom  7129  findcard2  7159  findcard2s  7160  fimax2gtrilemstep  7171  undifdcss  7196  tpfidceq  7203  fipwssg  7279  2omap  7282  supelti  7306  nlt1pig  7672  dfplpq2  7685  ltsonq  7729  archnqq  7748  nqnq0pi  7769  prarloclemn  7830  genprndl  7852  genprndu  7853  genpdisj  7854  addlocprlemgt  7865  addlocpr  7867  nqprl  7882  nqpru  7883  addnqprlemrl  7888  addnqprlemru  7889  mulnqprlemrl  7904  mulnqprlemru  7905  ltpopr  7926  ltexprlemloc  7938  ltexprlemrl  7941  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  caucvgprlemladdfu  8008  suplocexprlemru  8050  axcaucvglemres  8230  cnegex  8467  mullt0  8771  eqord1  8774  mulge0  8910  divap0  8975  div2negap  9026  prodgt0  9143  ltmul12a  9151  recgt1i  9189  div4p1lem1div2  9509  nn0lt2  9677  peano5uzti  9704  btwnapz  9726  eluzp1m1  9896  eluzaddi  9899  eluzsubi  9900  uz2m1nn  9955  rphalflt  10034  xleaddadd  10239  ixxdisj  10255  iccgelb  10284  icodisj  10344  iccf1o  10357  fzsuc2  10435  fzonmapblen  10548  zsupcllemstep  10611  nninfdcex  10621  flqge0nn0  10677  flqge1nn  10678  modfzo0difsn  10781  nninfinf  10829  seqf1oglem2  10906  expubnd  10982  bernneq  11047  bernneq2  11048  nn0opthlem2d  11108  facwordi  11127  bcpasc  11153  hashnncl  11183  ccatsymb  11315  ccatass  11321  ccat1st1st  11354  fzowrddc  11364  swrdlend  11375  swrdfv2  11380  swrdspsleq  11384  pfxeq  11413  pfxsuff1eqwrdeq  11416  swrdswrdlem  11421  swrdswrd  11422  swrdpfx  11424  ccats1pfxeqrex  11432  pfxccatin12lem1  11445  swrdccatin2  11446  recvguniq  11705  sqrt0rlem  11713  resqrexlemover  11720  resqrexlemcalc3  11726  resqrexlemgt0  11730  resqrexlemoverl  11731  recvalap  11807  nnabscl  11810  negfi  11938  2zinfmin  11953  climi0  11999  climge0  12035  summodclem3  12091  fsumsplit  12118  fisumcom2  12149  fisumrev2  12157  explecnv  12216  cvgratnnlemseq  12237  fprodsplitdc  12307  fprodsplit  12308  fprodcom2fi  12337  eftlub  12401  sin02gt0  12475  dvdslelemd  12554  dvdsleabs2  12557  mulmoddvds  12574  odd2np1  12584  oexpneg  12588  mod2eq1n2dvds  12590  sqoddm1div8z  12597  rplpwr  12748  rppwr  12749  nn0seqcvgd  12763  lcmneg  12796  qredeq  12818  dvdsnprmd  12847  oddprmge3  12857  oddpwdclemdvds  12892  oddpwdclemndvds  12893  oddpwdclemodd  12894  znege1  12900  qgt0numnn  12921  phibndlem  12938  hashgcdeq  12962  reumodprminv  12976  coprimeprodsq2  12981  pythagtrip  13006  pceq0  13045  dvdsprmpweqle  13060  fldivp1  13071  4sqlem9  13109  4sqlem15  13128  4sqlem16  13129  ballotfilemfrcn0  13217  ennnfonelemf1  13253  imasmnd  13708  imasgrp  13864  subginv  13934  subgmulg  13941  eqger  13977  kerf1ghm  14027  rngpropd  14194  rng1zrlem  14198  srgidmlem  14221  ringpropd  14281  crngpropd  14282  imasring  14307  rhmf1o  14413  subrngpropd  14462  subrg1  14477  subrgpropd  14499  rrgnz  14515  aprsym  14534  aprcotr  14535  aprlring  14538  lmodprop2d  14622  lssssg  14634  lss0cl  14643  isridlrng  14756  rspcl  14765  rspssid  14766  rnglidlmmgm  14770  psrbagfsupp  14945  psrgrp  14966  mplsubgfilemcl  14980  neiuni  15152  neissex  15156  tgrest  15160  tgcnp  15200  lmfpm  15234  lmcl  15236  lmss  15237  lmff  15240  psmetdmdm  15315  xmeter  15427  neibl  15482  xmettxlem  15500  tgqioo  15546  cnopnap  15602  limcimo  15656  dvidsslem  15684  sinq12gt0  15821  logrpap0  15868  pellexlem2  15972  mersenne  15991  lgsdilem  16026  lgsdinn0  16047  gausslemma2dlem0b  16049  gausslemma2dlem1a  16057  gausslemma2dlem5  16065  gausslemma2dlem6  16066  lgsquad3  16083  m1lgs  16084  2lgslem1a  16087  2lgslem1  16090  2lgslem3a1  16096  2lgslem3b1  16097  2lgslem3c1  16098  2lgslem3d1  16099  2sqlem6  16119  edgupgren  16262  upgredg  16265  wlkl1loop  16479  wlk1walkdom  16480  upgriswlkdc  16481  loopclwwlkn1b  16540  eupth2lembfi  16598  isomninnlem  16940  ismkvnnlem  16963