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

Theorem biimpa 290
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 142 . 2 (𝜑 → (𝜓𝜒))
32imp 122 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  simprbda  375  simplbda  376  pm5.1  566  bimsc1  905  biimp3a  1277  equsex  1658  euor  1969  euan  1999  cgsexg  2645  cgsex2g  2646  cgsex4g  2647  ceqsex  2648  sbciegft  2855  sbeqalb  2881  syl5sseq  3058  euotd  4045  ralxfr2d  4250  rexxfr2d  4251  nlimsucg  4345  wetriext  4355  relop  4544  resiexg  4714  iotass  4951  fnbr  5069  f1o00  5236  fnex  5459  foelrn  5471  acexmidlemab  5585  f1ocnv2d  5783  ofrval  5801  eloprabi  5901  1stconst  5921  2ndconst  5922  poxp  5932  smodm2  5992  smoiso  5999  nnsucuniel  6188  erth  6266  iinerm  6294  phplem4dom  6508  findcard2  6535  findcard2s  6536  undifdcss  6560  supelti  6604  nlt1pig  6803  dfplpq2  6816  ltsonq  6860  archnqq  6879  nqnq0pi  6900  prarloclemn  6961  genprndl  6983  genprndu  6984  genpdisj  6985  addlocprlemgt  6996  addlocpr  6998  nqprl  7013  nqpru  7014  addnqprlemrl  7019  addnqprlemru  7020  mulnqprlemrl  7035  mulnqprlemru  7036  ltpopr  7057  ltexprlemloc  7069  ltexprlemrl  7072  cauappcvgprlemladdfu  7116  cauappcvgprlemladdfl  7117  caucvgprlemladdfu  7139  axcaucvglemres  7337  cnegex  7563  mullt0  7861  mulge0  7996  divap0  8049  div2negap  8100  prodgt0  8207  ltmul12a  8215  recgt1i  8253  div4p1lem1div2  8561  nn0lt2  8724  peano5uzti  8750  eluzp1m1  8937  eluzaddi  8940  eluzsubi  8941  uz2m1nn  8987  rphalflt  9058  ixxdisj  9216  iccgelb  9245  icodisj  9304  iccf1o  9316  fzsuc2  9386  fzonmapblen  9487  flqge0nn0  9589  flqge1nn  9590  modfzo0difsn  9691  expubnd  9849  bernneq  9909  bernneq2  9910  nn0opthlem2d  9964  facwordi  9983  bcpasc  10009  hashnncl  10039  recvguniq  10255  sqrt0rlem  10263  resqrexlemover  10270  resqrexlemcalc3  10276  resqrexlemgt0  10280  resqrexlemoverl  10281  recvalap  10357  nnabscl  10360  negfi  10484  climi0  10502  climge0  10537  dvdslelemd  10624  dvdsleabs2  10627  mulmoddvds  10644  odd2np1  10653  oexpneg  10657  mod2eq1n2dvds  10659  sqoddm1div8z  10666  zsupcllemstep  10721  rplpwr  10796  rppwr  10797  nn0seqcvgd  10803  lcmneg  10836  qredeq  10858  dvdsnprmd  10887  oddprmge3  10896  oddpwdclemdvds  10928  oddpwdclemndvds  10929  oddpwdclemodd  10930  znege1  10936  qgt0numnn  10957  phibndlem  10972  hashgcdeq  10984
  Copyright terms: Public domain W3C validator