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

Theorem 3impb 1162
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3impb.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
3impb ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem 3impb
StepHypRef Expression
1 3impb.1 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
21exp32 362 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1160 1 ((𝜑𝜓𝜒) → 𝜃)
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:  3adant1l  1193  3adant1r  1194  3impdi  1256  vtocl3gf  2723  rspc2ev  2778  reuss  3327  trssord  4272  funtp  5146  resdif  5357  funimass4  5440  fnovex  5772  fnotovb  5782  fovrn  5881  fnovrn  5886  fmpoco  6081  nndi  6350  nnaordi  6372  ecovass  6506  ecoviass  6507  ecovdi  6508  ecovidi  6509  eqsupti  6851  addasspig  7106  mulasspig  7108  distrpig  7109  distrnq0  7235  addassnq0  7238  distnq0r  7239  prcdnql  7260  prcunqu  7261  genpassl  7300  genpassu  7301  genpassg  7302  distrlem1prl  7358  distrlem1pru  7359  ltexprlemopl  7377  ltexprlemopu  7379  le2tri3i  7840  cnegexlem1  7905  subadd  7933  addsub  7941  subdi  8115  submul2  8129  div12ap  8422  diveqap1  8433  divnegap  8434  divdivap2  8452  ltmulgt11  8590  gt0div  8596  ge0div  8597  uzind3  9132  fnn0ind  9135  qdivcl  9403  irrmul  9407  xrlttr  9549  fzen  9791  lenegsq  10835  moddvds  11429  dvds2add  11454  dvds2sub  11455  dvdsleabs  11470  divalgb  11549  ndvdsadd  11555  modgcd  11606  absmulgcd  11632  setsresg  11924  unopn  12099  innei  12259  cncfi  12661
  Copyright terms: Public domain W3C validator