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

Theorem 3impb 1111
 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 351 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1109 1 ((𝜑𝜓𝜒) → 𝜃)
 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  2686  reuss  3245  trssord  4144  funtp  4979  resdif  5175  funimass4  5251  fnovex  5565  fnotovb  5575  fovrn  5670  fnovrn  5675  fmpt2co  5864  nndi  6095  nnaordi  6111  ecovass  6245  ecoviass  6246  ecovdi  6247  ecovidi  6248  eqsupti  6401  addasspig  6485  mulasspig  6487  distrpig  6488  distrnq0  6614  addassnq0  6617  distnq0r  6618  prcdnql  6639  prcunqu  6640  genpassl  6679  genpassu  6680  genpassg  6681  distrlem1prl  6737  distrlem1pru  6738  ltexprlemopl  6756  ltexprlemopu  6758  le2tri3i  7184  cnegexlem1  7248  subadd  7276  addsub  7284  subdi  7453  submul2  7467  div12ap  7746  diveqap1  7755  divnegap  7756  divdivap2  7774  ltmulgt11  7904  gt0div  7910  ge0div  7911  uzind3  8409  fnn0ind  8412  qdivcl  8674  irrmul  8678  xrlttr  8816  fzen  9008  iseqval  9383  lenegsq  9921  moddvds  10116  dvds2add  10140  dvds2sub  10141  dvdsleabs  10156
 Copyright terms: Public domain W3C validator