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  966  biimp3a  1358  equsex  1752  euor  2081  euan  2112  cgsexg  2812  cgsex2g  2813  cgsex4g  2814  ceqsex  2815  sbciegft  3036  sbeqalb  3062  sseqtrid  3251  exmidn0m  4261  euotd  4317  ralxfr2d  4529  rexxfr2d  4530  nlimsucg  4632  wetriext  4643  relop  4846  resiexg  5023  iotass  5268  fnbr  5397  f1o00  5580  foelcdmi  5654  fnex  5829  foelrn  5844  acexmidlemab  5961  f1ocnv2d  6173  ofrval  6192  eloprabi  6305  1stconst  6330  2ndconst  6331  poxp  6341  smodm2  6404  smoiso  6411  nnsucuniel  6604  erth  6689  iinerm  6717  pw2f1odclem  6956  pw2f1odc  6957  phplem4dom  6984  findcard2  7012  findcard2s  7013  fimax2gtrilemstep  7023  undifdcss  7046  tpfidceq  7053  fipwssg  7107  supelti  7130  nlt1pig  7489  dfplpq2  7502  ltsonq  7546  archnqq  7565  nqnq0pi  7586  prarloclemn  7647  genprndl  7669  genprndu  7670  genpdisj  7671  addlocprlemgt  7682  addlocpr  7684  nqprl  7699  nqpru  7700  addnqprlemrl  7705  addnqprlemru  7706  mulnqprlemrl  7721  mulnqprlemru  7722  ltpopr  7743  ltexprlemloc  7755  ltexprlemrl  7758  cauappcvgprlemladdfu  7802  cauappcvgprlemladdfl  7803  caucvgprlemladdfu  7825  suplocexprlemru  7867  axcaucvglemres  8047  cnegex  8285  mullt0  8588  eqord1  8591  mulge0  8727  divap0  8792  div2negap  8843  prodgt0  8960  ltmul12a  8968  recgt1i  9006  div4p1lem1div2  9326  nn0lt2  9489  peano5uzti  9516  btwnapz  9538  eluzp1m1  9707  eluzaddi  9710  eluzsubi  9711  uz2m1nn  9761  rphalflt  9840  xleaddadd  10044  ixxdisj  10060  iccgelb  10089  icodisj  10149  iccf1o  10161  fzsuc2  10236  fzonmapblen  10348  zsupcllemstep  10409  nninfdcex  10417  flqge0nn0  10473  flqge1nn  10474  modfzo0difsn  10577  nninfinf  10625  seqf1oglem2  10702  expubnd  10778  bernneq  10842  bernneq2  10843  nn0opthlem2d  10903  facwordi  10922  bcpasc  10948  hashnncl  10977  ccatsymb  11096  ccatass  11102  ccat1st1st  11131  fzowrddc  11138  swrdlend  11149  swrdfv2  11154  swrdspsleq  11158  pfxeq  11187  pfxsuff1eqwrdeq  11190  swrdswrdlem  11195  swrdswrd  11196  swrdpfx  11198  ccats1pfxeqrex  11206  pfxccatin12lem1  11219  swrdccatin2  11220  recvguniq  11421  sqrt0rlem  11429  resqrexlemover  11436  resqrexlemcalc3  11442  resqrexlemgt0  11446  resqrexlemoverl  11447  recvalap  11523  nnabscl  11526  negfi  11654  2zinfmin  11669  climi0  11715  climge0  11751  summodclem3  11806  fsumsplit  11833  fisumcom2  11864  fisumrev2  11872  explecnv  11931  cvgratnnlemseq  11952  fprodsplitdc  12022  fprodsplit  12023  fprodcom2fi  12052  eftlub  12116  sin02gt0  12190  dvdslelemd  12269  dvdsleabs2  12272  mulmoddvds  12289  odd2np1  12299  oexpneg  12303  mod2eq1n2dvds  12305  sqoddm1div8z  12312  rplpwr  12463  rppwr  12464  nn0seqcvgd  12478  lcmneg  12511  qredeq  12533  dvdsnprmd  12562  oddprmge3  12572  oddpwdclemdvds  12607  oddpwdclemndvds  12608  oddpwdclemodd  12609  znege1  12615  qgt0numnn  12636  phibndlem  12653  hashgcdeq  12677  reumodprminv  12691  coprimeprodsq2  12696  pythagtrip  12721  pceq0  12760  dvdsprmpweqle  12775  fldivp1  12786  4sqlem9  12824  4sqlem15  12843  4sqlem16  12844  ennnfonelemf1  12904  imasmnd  13400  imasgrp  13562  subginv  13632  subgmulg  13639  eqger  13675  kerf1ghm  13725  rngpropd  13832  srgidmlem  13855  srg1zr  13864  ringpropd  13915  crngpropd  13916  imasring  13941  rhmf1o  14045  subrngpropd  14093  subrg1  14108  subrgpropd  14130  rrgnz  14145  aprsym  14161  aprcotr  14162  lmodprop2d  14225  lssssg  14237  lss0cl  14246  isridlrng  14359  rspcl  14368  rspssid  14369  rnglidlmmgm  14373  psrgrp  14562  mplsubgfilemcl  14576  neiuni  14748  neissex  14752  tgrest  14756  tgcnp  14796  lmfpm  14830  lmcl  14832  lmss  14833  lmff  14836  psmetdmdm  14911  xmeter  15023  neibl  15078  xmettxlem  15096  tgqioo  15142  cnopnap  15198  limcimo  15252  dvidsslem  15280  sinq12gt0  15417  logrpap0  15464  mersenne  15584  lgsdilem  15619  lgsdinn0  15640  gausslemma2dlem0b  15642  gausslemma2dlem1a  15650  gausslemma2dlem5  15658  gausslemma2dlem6  15659  lgsquad3  15676  m1lgs  15677  2lgslem1a  15680  2lgslem1  15683  2lgslem3a1  15689  2lgslem3b1  15690  2lgslem3c1  15691  2lgslem3d1  15692  2sqlem6  15712  edgupgren  15845  upgredg  15848  2omap  16132  isomninnlem  16171  ismkvnnlem  16193