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

Theorem 3imp 1160
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 949 . 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 947
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 949
This theorem is referenced by:  3impa  1161  3impb  1162  3impia  1163  3impib  1164  3com23  1172  3an1rs  1182  3imp1  1183  3impd  1184  syl3an2  1235  syl3an3  1236  3jao  1264  biimp3ar  1309  poxp  6097  tfrlemibxssdm  6192  tfr1onlembxssdm  6208  tfrcllembxssdm  6221  nndi  6350  nnmass  6351  pr2nelem  7015  xnn0lenn0nn0  9616  difelfzle  9879  fzo1fzo0n0  9928  elfzo0z  9929  fzofzim  9933  elfzodifsumelfzo  9946  mulexp  10300  expadd  10303  expmul  10306  bernneq  10380  facdiv  10452  addmodlteqALT  11484  ltoddhalfle  11517  halfleoddlt  11518  dfgcd2  11629  cncongr1  11711  oddprmgt2  11741  prmfac1  11757  fiinopn  12098  opnneissb  12251  blssps  12523  blss  12524
  Copyright terms: Public domain W3C validator