Theorem 3impb 1189

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 363	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1183	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 968

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 970

This theorem is referenced by:  3adant1l  1220  3adant1r  1221  3impdi  1283  vtocl3gf  2789  rspc2ev  2845  reuss  3403  trssord  4358  funtp  5241  resdif  5454  funimass4  5537  fnovex  5875  fnotovb  5885  fovrn  5984  fnovrn  5989  fmpoco  6184  nndi  6454  nnaordi  6476  ecovass  6610  ecoviass  6611  ecovdi  6612  ecovidi  6613  eqsupti  6961  addasspig  7271  mulasspig  7273  distrpig  7274  distrnq0  7400  addassnq0  7403  distnq0r  7404  prcdnql  7425  prcunqu  7426  genpassl  7465  genpassu  7466  genpassg  7467  distrlem1prl  7523  distrlem1pru  7524  ltexprlemopl  7542  ltexprlemopu  7544  le2tri3i  8007  cnegexlem1  8073  subadd  8101  addsub  8109  subdi  8283  submul2  8297  div12ap  8590  diveqap1  8601  divnegap  8602  divdivap2  8620  ltmulgt11  8759  gt0div  8765  ge0div  8766  uzind3  9304  fnn0ind  9307  qdivcl  9581  irrmul  9585  xrlttr  9731  fzen  9978  lenegsq  11037  moddvds  11739  dvds2add  11765  dvds2sub  11766  dvdsleabs  11783  divalgb  11862  ndvdsadd  11868  modgcd  11924  absmulgcd  11950  odzval  12173  pcmul  12233  setsresg  12432  unopn  12643  innei  12803  cncfi  13205