Theorem 3impb 1194

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 1188	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 975

This theorem is referenced by:  3adant1l  1225  3adant1r  1226  3impdi  1288  vtocl3gf  2793  rspc2ev  2849  reuss  3408  trssord  4363  funtp  5249  resdif  5462  funimass4  5545  fnovex  5884  fnotovb  5894  fovrn  5993  fnovrn  5998  fmpoco  6193  nndi  6463  nnaordi  6485  ecovass  6620  ecoviass  6621  ecovdi  6622  ecovidi  6623  eqsupti  6971  addasspig  7285  mulasspig  7287  distrpig  7288  distrnq0  7414  addassnq0  7417  distnq0r  7418  prcdnql  7439  prcunqu  7440  genpassl  7479  genpassu  7480  genpassg  7481  distrlem1prl  7537  distrlem1pru  7538  ltexprlemopl  7556  ltexprlemopu  7558  le2tri3i  8021  cnegexlem1  8087  subadd  8115  addsub  8123  subdi  8297  submul2  8311  div12ap  8604  diveqap1  8615  divnegap  8616  divdivap2  8634  ltmulgt11  8773  gt0div  8779  ge0div  8780  uzind3  9318  fnn0ind  9321  qdivcl  9595  irrmul  9599  xrlttr  9745  fzen  9992  lenegsq  11052  moddvds  11754  dvds2add  11780  dvds2sub  11781  dvdsleabs  11798  divalgb  11877  ndvdsadd  11883  modgcd  11939  absmulgcd  11965  odzval  12188  pcmul  12248  setsresg  12447  submcl  12694  unopn  12762  innei  12922  cncfi  13324