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  bimsc1  963  biimp3a  1345  equsex  1728  euor  2052  euan  2082  cgsexg  2772  cgsex2g  2773  cgsex4g  2774  ceqsex  2775  sbciegft  2993  sbeqalb  3019  sseqtrid  3205  exmidn0m  4201  euotd  4254  ralxfr2d  4464  rexxfr2d  4465  nlimsucg  4565  wetriext  4576  relop  4777  resiexg  4952  iotass  5195  fnbr  5318  f1o00  5496  foelcdmi  5568  fnex  5738  foelrn  5753  acexmidlemab  5868  f1ocnv2d  6074  ofrval  6092  eloprabi  6196  1stconst  6221  2ndconst  6222  poxp  6232  smodm2  6295  smoiso  6302  nnsucuniel  6495  erth  6578  iinerm  6606  phplem4dom  6861  findcard2  6888  findcard2s  6889  fimax2gtrilemstep  6899  undifdcss  6921  fipwssg  6977  supelti  7000  nlt1pig  7339  dfplpq2  7352  ltsonq  7396  archnqq  7415  nqnq0pi  7436  prarloclemn  7497  genprndl  7519  genprndu  7520  genpdisj  7521  addlocprlemgt  7532  addlocpr  7534  nqprl  7549  nqpru  7550  addnqprlemrl  7555  addnqprlemru  7556  mulnqprlemrl  7571  mulnqprlemru  7572  ltpopr  7593  ltexprlemloc  7605  ltexprlemrl  7608  cauappcvgprlemladdfu  7652  cauappcvgprlemladdfl  7653  caucvgprlemladdfu  7675  suplocexprlemru  7717  axcaucvglemres  7897  cnegex  8134  mullt0  8436  eqord1  8439  mulge0  8575  divap0  8640  div2negap  8691  prodgt0  8808  ltmul12a  8816  recgt1i  8854  div4p1lem1div2  9171  nn0lt2  9333  peano5uzti  9360  btwnapz  9382  eluzp1m1  9550  eluzaddi  9553  eluzsubi  9554  uz2m1nn  9604  rphalflt  9682  xleaddadd  9886  ixxdisj  9902  iccgelb  9931  icodisj  9991  iccf1o  10003  fzsuc2  10078  fzonmapblen  10186  flqge0nn0  10292  flqge1nn  10293  modfzo0difsn  10394  expubnd  10576  bernneq  10640  bernneq2  10641  nn0opthlem2d  10700  facwordi  10719  bcpasc  10745  hashnncl  10774  recvguniq  11003  sqrt0rlem  11011  resqrexlemover  11018  resqrexlemcalc3  11024  resqrexlemgt0  11028  resqrexlemoverl  11029  recvalap  11105  nnabscl  11108  negfi  11235  2zinfmin  11250  climi0  11296  climge0  11332  summodclem3  11387  fsumsplit  11414  fisumcom2  11445  fisumrev2  11453  explecnv  11512  cvgratnnlemseq  11533  fprodsplitdc  11603  fprodsplit  11604  fprodcom2fi  11633  eftlub  11697  sin02gt0  11770  dvdslelemd  11848  dvdsleabs2  11851  mulmoddvds  11868  odd2np1  11877  oexpneg  11881  mod2eq1n2dvds  11883  sqoddm1div8z  11890  zsupcllemstep  11945  nninfdcex  11953  rplpwr  12027  rppwr  12028  nn0seqcvgd  12040  lcmneg  12073  qredeq  12095  dvdsnprmd  12124  oddprmge3  12134  oddpwdclemdvds  12169  oddpwdclemndvds  12170  oddpwdclemodd  12171  znege1  12177  qgt0numnn  12198  phibndlem  12215  hashgcdeq  12238  reumodprminv  12252  coprimeprodsq2  12257  pythagtrip  12282  pceq0  12320  dvdsprmpweqle  12335  fldivp1  12345  4sqlem9  12383  ennnfonelemf1  12418  subginv  13039  subgmulg  13046  eqger  13081  srgidmlem  13159  srg1zr  13168  ringpropd  13215  crngpropd  13216  aprsym  13340  aprcotr  13341  subrg1  13357  subrgpropd  13374  neiuni  13597  neissex  13601  tgrest  13605  tgcnp  13645  lmfpm  13679  lmcl  13681  lmss  13682  lmff  13685  psmetdmdm  13760  xmeter  13872  neibl  13927  xmettxlem  13945  tgqioo  13983  cnopnap  14030  limcimo  14070  sinq12gt0  14187  logrpap0  14234  lgsdilem  14364  lgsdinn0  14385  m1lgs  14388  2sqlem6  14403  isomninnlem  14714  ismkvnnlem  14736