Theorem 3expb 1182

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 1180	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 255	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

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

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 964

This theorem is referenced by:  3adant3r1  1190  3adant3r2  1191  3adant3r3  1192  3adant1l  1208  3adant1r  1209  mp3an1  1302  soinxp  4604  sotri  4929  fnfco  5292  mpoeq3dva  5828  fovrnda  5907  ovelrn  5912  grprinvd  5959  fnmpoovd  6105  nnmsucr  6377  fidifsnid  6758  exmidpw  6795  undiffi  6806  fidcenumlemim  6833  ltpopr  7396  ltexprlemdisj  7407  recexprlemdisj  7431  mul4  7887  add4  7916  2addsub  7969  addsubeq4  7970  subadd4  7999  muladd  8139  ltleadd  8201  divmulap  8428  divap0  8437  div23ap  8444  div12ap  8447  divsubdirap  8461  divcanap5  8467  divmuleqap  8470  divcanap6  8472  divdiv32ap  8473  div2subap  8589  letrp1  8599  lemul12b  8612  lediv1  8620  cju  8712  nndivre  8749  nndivtr  8755  nn0addge1  9016  nn0addge2  9017  peano2uz2  9151  uzind  9155  uzind3  9157  fzind  9159  fnn0ind  9160  uzind4  9376  qre  9410  irrmul  9432  rpdivcl  9460  rerpdivcl  9465  iccshftr  9770  iccshftl  9772  iccdil  9774  icccntr  9776  fzaddel  9832  fzrev  9857  frec2uzf1od  10172  expdivap  10337  2shfti  10596  iooinsup  11039  isermulc2  11102  dvds2add  11516  dvds2sub  11517  dvdstr  11519  alzdvds  11541  divalg2  11612  lcmgcdlem  11747  lcmgcdeq  11753  isprm6  11814  tgclb  12223  topbas  12225  neissex  12323  cnpnei  12377  txcnp  12429  psmetxrge0  12490  psmetlecl  12492  xmetlecl  12525  xmettpos  12528  elbl3ps  12552  elbl3  12553  metss  12652  comet  12657  bdxmet  12659  bdmet  12660  bl2ioo  12700  divcnap  12713  cncffvrn  12727  divccncfap  12735  dvrecap  12835  cosz12  12850