Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  3imp Unicode version

Theorem 3imp 1176
 Description: Importation inference. (Contributed by NM, 8-Apr-1994.)
Hypothesis
Ref Expression
3imp.1
Assertion
Ref Expression
3imp

Proof of Theorem 3imp
StepHypRef Expression
1 df-3an 965 . 2
2 3imp.1 . . 3
32imp31 254 . 2
41, 3sylbi 120 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   w3a 963 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  df-3an 965 This theorem is referenced by:  3impa  1177  3impb  1178  3impia  1179  3impib  1180  3com23  1188  3an1rs  1198  3imp1  1199  3impd  1200  syl3an2  1251  syl3an3  1252  3jao  1280  biimp3ar  1325  poxp  6169  tfrlemibxssdm  6264  tfr1onlembxssdm  6280  tfrcllembxssdm  6293  nndi  6422  nnmass  6423  pr2nelem  7105  xnn0lenn0nn0  9747  difelfzle  10011  fzo1fzo0n0  10060  elfzo0z  10061  fzofzim  10065  elfzodifsumelfzo  10078  mulexp  10436  expadd  10439  expmul  10442  bernneq  10516  facdiv  10589  addmodlteqALT  11724  ltoddhalfle  11757  halfleoddlt  11758  dfgcd2  11869  cncongr1  11951  oddprmgt2  11981  prmfac1  11997  fiinopn  12341  opnneissb  12494  blssps  12766  blss  12767
 Copyright terms: Public domain W3C validator