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

Theorem 3impb 1111
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3impb.1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
3impb  |-  ( (
ph  /\  ps  /\  ch )  ->  th )

Proof of Theorem 3impb
StepHypRef Expression
1 3impb.1 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
21exp32 351 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1109 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    /\ w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  3adant1l  1138  3adant1r  1139  3impdi  1201  vtocl3gf  2633  rspc2ev  2687  reuss  3246  trssord  4145  funtp  4980  resdif  5176  funimass4  5252  fnovex  5566  fnotovb  5576  fovrn  5671  fnovrn  5676  fmpt2co  5865  nndi  6096  nnaordi  6112  ecovass  6246  ecoviass  6247  ecovdi  6248  ecovidi  6249  eqsupti  6402  addasspig  6486  mulasspig  6488  distrpig  6489  distrnq0  6615  addassnq0  6618  distnq0r  6619  prcdnql  6640  prcunqu  6641  genpassl  6680  genpassu  6681  genpassg  6682  distrlem1prl  6738  distrlem1pru  6739  ltexprlemopl  6757  ltexprlemopu  6759  le2tri3i  7185  cnegexlem1  7249  subadd  7277  addsub  7285  subdi  7454  submul2  7468  div12ap  7747  diveqap1  7756  divnegap  7757  divdivap2  7775  ltmulgt11  7905  gt0div  7911  ge0div  7912  uzind3  8410  fnn0ind  8413  qdivcl  8675  irrmul  8679  xrlttr  8817  fzen  9009  iseqval  9384  lenegsq  9922  moddvds  10117  dvds2add  10141  dvds2sub  10142  dvdsleabs  10157  divalgb  10237  ndvdsadd  10243
  Copyright terms: Public domain W3C validator