Theorem 3impb 1137

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

Step	Hyp	Ref	Expression
1		3impb.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	exp32 357	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1135	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 922

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 924

This theorem is referenced by:  3adant1l  1164  3adant1r  1165  3impdi  1227  vtocl3gf  2675  rspc2ev  2728  reuss  3269  trssord  4183  funtp  5034  resdif  5240  funimass4  5320  fnovex  5641  fnotovb  5651  fovrn  5746  fnovrn  5751  fmpt2co  5940  nndi  6203  nnaordi  6221  ecovass  6355  ecoviass  6356  ecovdi  6357  ecovidi  6358  eqsupti  6638  addasspig  6836  mulasspig  6838  distrpig  6839  distrnq0  6965  addassnq0  6968  distnq0r  6969  prcdnql  6990  prcunqu  6991  genpassl  7030  genpassu  7031  genpassg  7032  distrlem1prl  7088  distrlem1pru  7089  ltexprlemopl  7107  ltexprlemopu  7109  le2tri3i  7540  cnegexlem1  7604  subadd  7632  addsub  7640  subdi  7810  submul2  7824  div12ap  8103  diveqap1  8114  divnegap  8115  divdivap2  8133  ltmulgt11  8263  gt0div  8269  ge0div  8270  uzind3  8795  fnn0ind  8798  qdivcl  9063  irrmul  9067  xrlttr  9200  fzen  9392  iseqval  9802  lenegsq  10445  moddvds  10730  dvds2add  10755  dvds2sub  10756  dvdsleabs  10771  divalgb  10850  ndvdsadd  10856  modgcd  10907  absmulgcd  10931