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

Theorem 3impb 1178
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 363 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1176 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 963
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 965
This theorem is referenced by:  3adant1l  1209  3adant1r  1210  3impdi  1272  vtocl3gf  2752  rspc2ev  2807  reuss  3361  trssord  4309  funtp  5183  resdif  5396  funimass4  5479  fnovex  5811  fnotovb  5821  fovrn  5920  fnovrn  5925  fmpoco  6120  nndi  6389  nnaordi  6411  ecovass  6545  ecoviass  6546  ecovdi  6547  ecovidi  6548  eqsupti  6890  addasspig  7161  mulasspig  7163  distrpig  7164  distrnq0  7290  addassnq0  7293  distnq0r  7294  prcdnql  7315  prcunqu  7316  genpassl  7355  genpassu  7356  genpassg  7357  distrlem1prl  7413  distrlem1pru  7414  ltexprlemopl  7432  ltexprlemopu  7434  le2tri3i  7895  cnegexlem1  7960  subadd  7988  addsub  7996  subdi  8170  submul2  8184  div12ap  8477  diveqap1  8488  divnegap  8489  divdivap2  8507  ltmulgt11  8645  gt0div  8651  ge0div  8652  uzind3  9187  fnn0ind  9190  qdivcl  9461  irrmul  9465  xrlttr  9610  fzen  9853  lenegsq  10898  moddvds  11536  dvds2add  11561  dvds2sub  11562  dvdsleabs  11577  divalgb  11656  ndvdsadd  11662  modgcd  11713  absmulgcd  11739  setsresg  12034  unopn  12209  innei  12369  cncfi  12771
  Copyright terms: Public domain W3C validator