ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimpa GIF version

Theorem biimpa 294
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
StepHypRef Expression
1 biimpa.1 . . 3 (𝜑 → (𝜓𝜒))
21biimpd 143 . 2 (𝜑 → (𝜓𝜒))
32imp 123 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  simprbda  380  simplbda  381  pm5.1  590  bimsc1  947  biimp3a  1323  equsex  1706  euor  2025  euan  2055  cgsexg  2721  cgsex2g  2722  cgsex4g  2723  ceqsex  2724  sbciegft  2939  sbeqalb  2965  sseqtrid  3147  exmidn0m  4124  euotd  4176  ralxfr2d  4385  rexxfr2d  4386  nlimsucg  4481  wetriext  4491  relop  4689  resiexg  4864  iotass  5105  fnbr  5225  f1o00  5402  fnex  5642  foelrn  5654  acexmidlemab  5768  f1ocnv2d  5974  ofrval  5992  eloprabi  6094  1stconst  6118  2ndconst  6119  poxp  6129  smodm2  6192  smoiso  6199  nnsucuniel  6391  erth  6473  iinerm  6501  phplem4dom  6756  findcard2  6783  findcard2s  6784  fimax2gtrilemstep  6794  undifdcss  6811  fipwssg  6867  supelti  6889  nlt1pig  7156  dfplpq2  7169  ltsonq  7213  archnqq  7232  nqnq0pi  7253  prarloclemn  7314  genprndl  7336  genprndu  7337  genpdisj  7338  addlocprlemgt  7349  addlocpr  7351  nqprl  7366  nqpru  7367  addnqprlemrl  7372  addnqprlemru  7373  mulnqprlemrl  7388  mulnqprlemru  7389  ltpopr  7410  ltexprlemloc  7422  ltexprlemrl  7425  cauappcvgprlemladdfu  7469  cauappcvgprlemladdfl  7470  caucvgprlemladdfu  7492  suplocexprlemru  7534  axcaucvglemres  7714  cnegex  7947  mullt0  8249  eqord1  8252  mulge0  8388  divap0  8451  div2negap  8502  prodgt0  8617  ltmul12a  8625  recgt1i  8663  div4p1lem1div2  8980  nn0lt2  9139  peano5uzti  9166  btwnapz  9188  eluzp1m1  9356  eluzaddi  9359  eluzsubi  9360  uz2m1nn  9406  rphalflt  9478  xleaddadd  9677  ixxdisj  9693  iccgelb  9722  icodisj  9782  iccf1o  9794  fzsuc2  9866  fzonmapblen  9971  flqge0nn0  10073  flqge1nn  10074  modfzo0difsn  10175  expubnd  10357  bernneq  10419  bernneq2  10420  nn0opthlem2d  10474  facwordi  10493  bcpasc  10519  hashnncl  10549  recvguniq  10774  sqrt0rlem  10782  resqrexlemover  10789  resqrexlemcalc3  10795  resqrexlemgt0  10799  resqrexlemoverl  10800  recvalap  10876  nnabscl  10879  negfi  11006  climi0  11065  climge0  11101  summodclem3  11156  fsumsplit  11183  fisumcom2  11214  fisumrev2  11222  explecnv  11281  cvgratnnlemseq  11302  eftlub  11403  sin02gt0  11477  dvdslelemd  11548  dvdsleabs2  11551  mulmoddvds  11568  odd2np1  11577  oexpneg  11581  mod2eq1n2dvds  11583  sqoddm1div8z  11590  zsupcllemstep  11645  rplpwr  11722  rppwr  11723  nn0seqcvgd  11729  lcmneg  11762  qredeq  11784  dvdsnprmd  11813  oddprmge3  11822  oddpwdclemdvds  11855  oddpwdclemndvds  11856  oddpwdclemodd  11857  znege1  11863  qgt0numnn  11884  phibndlem  11899  hashgcdeq  11911  ennnfonelemf1  11938  neiuni  12340  neissex  12344  tgrest  12348  tgcnp  12388  lmfpm  12422  lmcl  12424  lmss  12425  lmff  12428  psmetdmdm  12503  xmeter  12615  neibl  12670  xmettxlem  12688  tgqioo  12726  cnopnap  12773  limcimo  12813  sinq12gt0  12921  isomninnlem  13239
  Copyright terms: Public domain W3C validator