Theorem 3expb 1105

Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expb	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem 3expb

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1103	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 244	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  3adant3r1  1113  3adant3r2  1114  3adant3r3  1115  3adant1l  1127  3adant1r  1128  mp3an1  1219  soinxp  4410  sotri  4720  fnfco  5065  mpt2eq3dva  5569  fovrnda  5644  ovelrn  5649  grprinvd  5696  nnmsucr  6067  ltpopr  6691  ltexprlemdisj  6702  recexprlemdisj  6726  mul4  7143  add4  7170  2addsub  7223  addsubeq4  7224  subadd4  7253  muladd  7379  ltleadd  7439  divmulap  7652  divap0  7661  div23ap  7668  div12ap  7671  divsubdirap  7682  divcanap5  7688  divmuleqap  7691  divcanap6  7693  divdiv32ap  7694  letrp1  7812  lemul12b  7825  lediv1  7833  cju  7911  nndivre  7947  nndivtr  7953  nn0addge1  8226  nn0addge2  8227  peano2uz2  8343  uzind  8347  uzind3  8349  fzind  8351  fnn0ind  8352  uzind4  8529  qre  8558  irrmul  8579  rpdivcl  8606  rerpdivcl  8611  iccshftr  8860  iccshftl  8862  iccdil  8864  icccntr  8866  fzaddel  8920  fzrev  8944  frec2uzf1od  9166  expdivap  9279  2shfti  9406  iisermulc2  9834