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  907  biimp3a  1279  equsex  1660  euor  1971  euan  2001  cgsexg  2648  cgsex2g  2649  cgsex4g  2650  ceqsex  2651  sbciegft  2858  sbeqalb  2884  syl5sseq  3063  euotd  4055  ralxfr2d  4260  rexxfr2d  4261  nlimsucg  4355  wetriext  4365  relop  4554  resiexg  4724  iotass  4963  fnbr  5081  f1o00  5251  fnex  5480  foelrn  5492  acexmidlemab  5607  f1ocnv2d  5805  ofrval  5823  eloprabi  5923  1stconst  5943  2ndconst  5944  poxp  5954  smodm2  6014  smoiso  6021  nnsucuniel  6210  erth  6288  iinerm  6316  phplem4dom  6530  findcard2  6557  findcard2s  6558  fimax2gtrilemstep  6568  undifdcss  6585  supelti  6641  nlt1pig  6844  dfplpq2  6857  ltsonq  6901  archnqq  6920  nqnq0pi  6941  prarloclemn  7002  genprndl  7024  genprndu  7025  genpdisj  7026  addlocprlemgt  7037  addlocpr  7039  nqprl  7054  nqpru  7055  addnqprlemrl  7060  addnqprlemru  7061  mulnqprlemrl  7076  mulnqprlemru  7077  ltpopr  7098  ltexprlemloc  7110  ltexprlemrl  7113  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  caucvgprlemladdfu  7180  axcaucvglemres  7378  cnegex  7604  mullt0  7902  mulge0  8037  divap0  8090  div2negap  8141  prodgt0  8248  ltmul12a  8256  recgt1i  8294  div4p1lem1div2  8602  nn0lt2  8761  peano5uzti  8787  eluzp1m1  8974  eluzaddi  8977  eluzsubi  8978  uz2m1nn  9024  rphalflt  9095  ixxdisj  9253  iccgelb  9282  icodisj  9341  iccf1o  9353  fzsuc2  9423  fzonmapblen  9526  flqge0nn0  9628  flqge1nn  9629  modfzo0difsn  9730  expubnd  9910  bernneq  9970  bernneq2  9971  nn0opthlem2d  10025  facwordi  10044  bcpasc  10070  hashnncl  10100  recvguniq  10323  sqrt0rlem  10331  resqrexlemover  10338  resqrexlemcalc3  10344  resqrexlemgt0  10348  resqrexlemoverl  10349  recvalap  10425  nnabscl  10428  negfi  10552  climi0  10570  climge0  10605  isummolem3  10659  dvdslelemd  10719  dvdsleabs2  10722  mulmoddvds  10739  odd2np1  10748  oexpneg  10752  mod2eq1n2dvds  10754  sqoddm1div8z  10761  zsupcllemstep  10816  rplpwr  10891  rppwr  10892  nn0seqcvgd  10898  lcmneg  10931  qredeq  10953  dvdsnprmd  10982  oddprmge3  10991  oddpwdclemdvds  11023  oddpwdclemndvds  11024  oddpwdclemodd  11025  znege1  11031  qgt0numnn  11052  phibndlem  11067  hashgcdeq  11079
  Copyright terms: Public domain W3C validator