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  1739  euor  2068  euan  2098  cgsexg  2795  cgsex2g  2796  cgsex4g  2797  ceqsex  2798  sbciegft  3017  sbeqalb  3043  sseqtrid  3230  exmidn0m  4231  euotd  4284  ralxfr2d  4496  rexxfr2d  4497  nlimsucg  4599  wetriext  4610  relop  4813  resiexg  4988  iotass  5233  fnbr  5357  f1o00  5536  foelcdmi  5610  fnex  5781  foelrn  5796  acexmidlemab  5913  f1ocnv2d  6124  ofrval  6143  eloprabi  6251  1stconst  6276  2ndconst  6277  poxp  6287  smodm2  6350  smoiso  6357  nnsucuniel  6550  erth  6635  iinerm  6663  pw2f1odclem  6892  pw2f1odc  6893  phplem4dom  6920  findcard2  6947  findcard2s  6948  fimax2gtrilemstep  6958  undifdcss  6981  fipwssg  7040  supelti  7063  nlt1pig  7403  dfplpq2  7416  ltsonq  7460  archnqq  7479  nqnq0pi  7500  prarloclemn  7561  genprndl  7583  genprndu  7584  genpdisj  7585  addlocprlemgt  7596  addlocpr  7598  nqprl  7613  nqpru  7614  addnqprlemrl  7619  addnqprlemru  7620  mulnqprlemrl  7635  mulnqprlemru  7636  ltpopr  7657  ltexprlemloc  7669  ltexprlemrl  7672  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  caucvgprlemladdfu  7739  suplocexprlemru  7781  axcaucvglemres  7961  cnegex  8199  mullt0  8501  eqord1  8504  mulge0  8640  divap0  8705  div2negap  8756  prodgt0  8873  ltmul12a  8881  recgt1i  8919  div4p1lem1div2  9239  nn0lt2  9401  peano5uzti  9428  btwnapz  9450  eluzp1m1  9619  eluzaddi  9622  eluzsubi  9623  uz2m1nn  9673  rphalflt  9752  xleaddadd  9956  ixxdisj  9972  iccgelb  10001  icodisj  10061  iccf1o  10073  fzsuc2  10148  fzonmapblen  10257  flqge0nn0  10365  flqge1nn  10366  modfzo0difsn  10469  nninfinf  10517  seqf1oglem2  10594  expubnd  10670  bernneq  10734  bernneq2  10735  nn0opthlem2d  10795  facwordi  10814  bcpasc  10840  hashnncl  10869  recvguniq  11142  sqrt0rlem  11150  resqrexlemover  11157  resqrexlemcalc3  11163  resqrexlemgt0  11167  resqrexlemoverl  11168  recvalap  11244  nnabscl  11247  negfi  11374  2zinfmin  11389  climi0  11435  climge0  11471  summodclem3  11526  fsumsplit  11553  fisumcom2  11584  fisumrev2  11592  explecnv  11651  cvgratnnlemseq  11672  fprodsplitdc  11742  fprodsplit  11743  fprodcom2fi  11772  eftlub  11836  sin02gt0  11910  dvdslelemd  11988  dvdsleabs2  11991  mulmoddvds  12008  odd2np1  12017  oexpneg  12021  mod2eq1n2dvds  12023  sqoddm1div8z  12030  zsupcllemstep  12085  nninfdcex  12093  rplpwr  12167  rppwr  12168  nn0seqcvgd  12182  lcmneg  12215  qredeq  12237  dvdsnprmd  12266  oddprmge3  12276  oddpwdclemdvds  12311  oddpwdclemndvds  12312  oddpwdclemodd  12313  znege1  12319  qgt0numnn  12340  phibndlem  12357  hashgcdeq  12380  reumodprminv  12394  coprimeprodsq2  12399  pythagtrip  12424  pceq0  12463  dvdsprmpweqle  12478  fldivp1  12489  4sqlem9  12527  4sqlem15  12546  4sqlem16  12547  ennnfonelemf1  12578  imasgrp  13184  subginv  13254  subgmulg  13261  eqger  13297  kerf1ghm  13347  rngpropd  13454  srgidmlem  13477  srg1zr  13486  ringpropd  13537  crngpropd  13538  imasring  13563  rhmf1o  13667  subrngpropd  13715  subrg1  13730  subrgpropd  13752  rrgnz  13767  aprsym  13783  aprcotr  13784  lmodprop2d  13847  lssssg  13859  lss0cl  13868  isridlrng  13981  rspcl  13990  rspssid  13991  rnglidlmmgm  13995  neiuni  14340  neissex  14344  tgrest  14348  tgcnp  14388  lmfpm  14422  lmcl  14424  lmss  14425  lmff  14428  psmetdmdm  14503  xmeter  14615  neibl  14670  xmettxlem  14688  tgqioo  14734  cnopnap  14790  limcimo  14844  dvidsslem  14872  sinq12gt0  15006  logrpap0  15053  lgsdilem  15184  lgsdinn0  15205  gausslemma2dlem0b  15207  gausslemma2dlem1a  15215  gausslemma2dlem5  15223  gausslemma2dlem6  15224  lgsquad3  15241  m1lgs  15242  2lgslem1a  15245  2lgslem1  15248  2lgslem3a1  15254  2lgslem3b1  15255  2lgslem3c1  15256  2lgslem3d1  15257  2sqlem6  15277  isomninnlem  15590  ismkvnnlem  15612