Theorem 3expb 1204

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 1202	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 257	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:  3adant3r1  1212  3adant3r2  1213  3adant3r3  1214  3adant1l  1230  3adant1r  1231  mp3an1  1324  soinxp  4697  sotri  5025  fnfco  5391  mpoeq3dva  5939  fovcdmda  6018  ovelrn  6023  fnmpoovd  6216  nnmsucr  6489  fidifsnid  6871  exmidpw  6908  undiffi  6924  fidcenumlemim  6951  ltpopr  7594  ltexprlemdisj  7605  recexprlemdisj  7629  mul4  8089  add4  8118  2addsub  8171  addsubeq4  8172  subadd4  8201  muladd  8341  ltleadd  8403  divmulap  8632  divap0  8641  div23ap  8648  div12ap  8651  divsubdirap  8665  divcanap5  8671  divmuleqap  8674  divcanap6  8676  divdiv32ap  8677  div2subap  8794  letrp1  8805  lemul12b  8818  lediv1  8826  cju  8918  nndivre  8955  nndivtr  8961  nn0addge1  9222  nn0addge2  9223  peano2uz2  9360  uzind  9364  uzind3  9366  fzind  9368  fnn0ind  9369  uzind4  9588  qre  9625  irrmul  9647  rpdivcl  9679  rerpdivcl  9684  iccshftr  9994  iccshftl  9996  iccdil  9998  icccntr  10000  fzaddel  10059  fzrev  10084  frec2uzf1od  10406  expdivap  10571  2shfti  10840  iooinsup  11285  isermulc2  11348  dvds2add  11832  dvds2sub  11833  dvdstr  11835  alzdvds  11860  divalg2  11931  lcmgcdlem  12077  lcmgcdeq  12083  isprm6  12147  pcqcl  12306  mgmplusf  12785  grprinvd  12805  ismndd  12838  idmhm  12860  issubm2  12864  submid  12868  0mhm  12873  mhmco  12874  mhmima  12875  grpinvcnv  12938  grpinvnzcl  12942  grpsubf  12949  mhmfmhm  12981  mulgnnsubcl  12995  mulgnn0z  13010  mulgnndir  13012  issubg4m  13053  isnsg3  13067  nsgid  13075  srgfcl  13156  srgmulgass  13172  srglmhm  13176  srgrmhm  13177  opprringbg  13250  mulgass3  13254  issubrg2  13362  islmodd  13383  lmodscaf  13400  lcomf  13417  rmodislmodlem  13440  tgclb  13568  topbas  13570  neissex  13668  cnpnei  13722  txcnp  13774  psmetxrge0  13835  psmetlecl  13837  xmetlecl  13870  xmettpos  13873  elbl3ps  13897  elbl3  13898  metss  13997  comet  14002  bdxmet  14004  bdmet  14005  bl2ioo  14045  divcnap  14058  cncfcdm  14072  divccncfap  14080  dvrecap  14180  cosz12  14204