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

Theorem biimpa 284
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 136 . 2 (𝜑 → (𝜓𝜒))
32imp 119 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  simprbda  369  simplbda  370  pm5.1  543  bimsc1  881  biimp3a  1251  equsex  1632  euor  1942  euan  1972  cgsexg  2606  cgsex2g  2607  cgsex4g  2608  ceqsex  2609  sbciegft  2815  sbeqalb  2841  syl5sseq  3020  euotd  4018  ralxfr2d  4223  rexxfr2d  4224  nlimsucg  4317  wetriext  4328  relop  4513  resiexg  4680  iotass  4911  fnbr  5028  f1o00  5188  fnex  5410  acexmidlemab  5533  f1ocnv2d  5731  ofrval  5749  eloprabi  5849  1stconst  5869  2ndconst  5870  poxp  5880  smodm2  5940  smoiso  5947  erth  6180  iinerm  6208  phplem4dom  6354  findcard2  6376  findcard2s  6377  nlt1pig  6496  dfplpq2  6509  ltsonq  6553  archnqq  6572  nqnq0pi  6593  prarloclemn  6654  genprndl  6676  genprndu  6677  genpdisj  6678  addlocprlemgt  6689  addlocpr  6691  nqprl  6706  nqpru  6707  addnqprlemrl  6712  addnqprlemru  6713  mulnqprlemrl  6728  mulnqprlemru  6729  ltpopr  6750  ltexprlemloc  6762  ltexprlemrl  6765  cauappcvgprlemladdfu  6809  cauappcvgprlemladdfl  6810  caucvgprlemladdfu  6832  axcaucvglemres  7030  cnegex  7251  mullt0  7548  mulge0  7683  divap0  7736  div2negap  7785  prodgt0  7892  ltmul12a  7900  recgt1i  7938  div4p1lem1div2  8234  nn0lt2  8379  peano5uzti  8404  eluzp1m1  8591  eluzaddi  8594  eluzsubi  8595  uz2m1nn  8638  rphalflt  8709  ixxdisj  8872  iccgelb  8901  icodisj  8960  iccf1o  8972  fzsuc2  9042  fzonmapblen  9144  flqge0nn0  9242  flqge1nn  9243  modfzo0difsn  9344  expubnd  9476  bernneq  9536  bernneq2  9537  nn0opthlem2d  9588  facwordi  9607  bcpasc  9633  recvguniq  9821  sqrt0rlem  9829  resqrexlemover  9836  resqrexlemcalc3  9842  resqrexlemgt0  9846  resqrexlemoverl  9847  recvalap  9923  nnabscl  9926  climi0  10040  climge0  10075  dvdslelemd  10154  dvdsleabs2  10157  mulmoddvds  10174  odd2np1  10183  oexpneg  10187  mod2eq1n2dvds  10190  sqoddm1div8z  10197  oddpwdclemdvds  10244  oddpwdclemndvds  10245  oddpwdclemodd  10246  nn0seqcvgd  10249
  Copyright terms: Public domain W3C validator