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

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

Proof of Theorem 3impa
StepHypRef Expression
1 3impa.1 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
21exp31 361 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1160 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  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  3impdir  1257  syl3an9b  1273  biimp3a  1308  stoic3  1392  rspec3  2499  rspc3v  2779  raltpg  3546  rextpg  3547  disjiun  3894  otexg  4122  opelopabt  4154  tpexg  4335  3optocl  4587  fun2ssres  5136  funssfv  5415  fvun1  5455  foco2  5623  f1elima  5642  eloprabga  5826  caovimo  5932  ot1stg  6018  ot2ndg  6019  ot3rdgg  6020  brtposg  6119  rdgexggg  6242  rdgivallem  6246  nnmass  6351  nndir  6354  nnaword  6375  th3q  6502  ecovass  6506  ecoviass  6507  fpmg  6536  findcard  6750  unfiin  6782  addasspig  7106  mulasspig  7108  mulcanpig  7111  ltapig  7114  ltmpig  7115  addassnqg  7158  ltbtwnnqq  7191  mulnnnq0  7226  addassnq0  7238  genpassl  7300  genpassu  7301  genpassg  7302  aptiprleml  7415  adddir  7725  le2tri3i  7840  addsub12  7943  subdir  8116  reapmul1  8325  recexaplem2  8381  div12ap  8422  divdiv32ap  8448  divdivap1  8451  lble  8673  zaddcllemneg  9061  fnn0ind  9135  xrltso  9550  iccgelb  9683  elicc4  9691  elfz  9764  fzrevral  9853  expnegap0  10269  expgt0  10294  expge0  10297  expge1  10298  mulexpzap  10301  expp1zap  10310  expm1ap  10311  abssubap0  10830  binom  11221  dvds0lem  11430  dvdsnegb  11437  muldvds1  11445  muldvds2  11446  divalgmodcl  11552  gcd2n0cl  11585  lcmdvds  11687  prmdvdsexp  11753  rpexp1i  11759  cnpval  12294  cnf2  12301  cnnei  12328  blssec  12534  blpnfctr  12535  mopni2  12579  mopni3  12580
  Copyright terms: Public domain W3C validator