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

Theorem 3imp 1158
Description: Importation inference. (Contributed by NM, 8-Apr-1994.)
Hypothesis
Ref Expression
3imp.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
3imp  |-  ( (
ph  /\  ps  /\  ch )  ->  th )

Proof of Theorem 3imp
StepHypRef Expression
1 df-3an 947 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
2 3imp.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 254 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3sylbi 120 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 945
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 947
This theorem is referenced by:  3impa  1159  3impb  1160  3impia  1161  3impib  1162  3com23  1170  3an1rs  1180  3imp1  1181  3impd  1182  syl3an2  1233  syl3an3  1234  3jao  1262  biimp3ar  1307  poxp  6095  tfrlemibxssdm  6190  tfr1onlembxssdm  6206  tfrcllembxssdm  6219  nndi  6348  nnmass  6349  pr2nelem  7013  xnn0lenn0nn0  9599  difelfzle  9862  fzo1fzo0n0  9911  elfzo0z  9912  fzofzim  9916  elfzodifsumelfzo  9929  mulexp  10283  expadd  10286  expmul  10289  bernneq  10363  facdiv  10435  addmodlteqALT  11464  ltoddhalfle  11497  halfleoddlt  11498  dfgcd2  11609  cncongr1  11691  oddprmgt2  11721  prmfac1  11737  fiinopn  12077  opnneissb  12230  blssps  12502  blss  12503
  Copyright terms: Public domain W3C validator