Theorem 3impb 1199

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  3adant1l  1230  3adant1r  1231  3impdi  1293  vtocl3gf  2802  rspc2ev  2858  reuss  3418  trssord  4382  funtp  5271  resdif  5485  funimass4  5568  fnovex  5910  fnotovb  5920  fovcdm  6019  fnovrn  6024  fmpoco  6219  nndi  6489  nnaordi  6511  ecovass  6646  ecoviass  6647  ecovdi  6648  ecovidi  6649  eqsupti  6997  addasspig  7331  mulasspig  7333  distrpig  7334  distrnq0  7460  addassnq0  7463  distnq0r  7464  prcdnql  7485  prcunqu  7486  genpassl  7525  genpassu  7526  genpassg  7527  distrlem1prl  7583  distrlem1pru  7584  ltexprlemopl  7602  ltexprlemopu  7604  le2tri3i  8068  cnegexlem1  8134  subadd  8162  addsub  8170  subdi  8344  submul2  8358  div12ap  8653  diveqap1  8664  divnegap  8665  divdivap2  8683  ltmulgt11  8823  gt0div  8829  ge0div  8830  uzind3  9368  fnn0ind  9371  qdivcl  9645  irrmul  9649  xrlttr  9797  fzen  10045  lenegsq  11106  moddvds  11808  dvds2add  11834  dvds2sub  11835  dvdsleabs  11853  divalgb  11932  ndvdsadd  11938  modgcd  11994  absmulgcd  12020  odzval  12243  pcmul  12303  setsresg  12502  issubmnd  12848  submcl  12875  grpinvid1  12929  grpinvid2  12930  mulgp1  13021  cmncom  13110  islss3  13471  unopn  13544  innei  13702  cncfi  14104