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

Theorem 3imp 1137
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 926 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
2 3imp.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 252 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3sylbi 119 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    /\ w3a 924
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  df-3an 926
This theorem is referenced by:  3impa  1138  3impb  1139  3impia  1140  3impib  1141  3com23  1149  3an1rs  1155  3imp1  1156  3impd  1157  syl3an2  1208  syl3an3  1209  3jao  1237  biimp3ar  1282  poxp  5979  tfrlemibxssdm  6074  tfr1onlembxssdm  6090  tfrcllembxssdm  6103  nndi  6229  nnmass  6230  pr2nelem  6798  difelfzle  9510  fzo1fzo0n0  9559  elfzo0z  9560  fzofzim  9564  elfzodifsumelfzo  9577  mulexp  9959  expadd  9962  expmul  9965  bernneq  10039  facdiv  10111  addmodlteqALT  10942  ltoddhalfle  10975  halfleoddlt  10976  dfgcd2  11085  cncongr1  11167  oddprmgt2  11197  prmfac1  11213
  Copyright terms: Public domain W3C validator