Theorem 3expa 1234

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

Hypothesis

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

Assertion

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

Proof of Theorem 3expa

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1233	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 256	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ad4ant123  1246  ad4ant124  1247  ad4ant134  1248  ad4ant234  1249  ad5ant123  1270  3anidm23  1338  mp3an2  1366  mpd3an3  1379  rgen3  2637  moi2  3007  sbc3ie  3125  2if2dc  3680  preq12bg  3898  issod  4464  wepo  4504  reuhypd  4617  funimass4  5753  fvtp1g  5923  f1imass  5980  fcof1o  5995  f1ofveu  6073  f1ocnvfv3  6074  acexmid  6084  2ndrn  6417  funsssuppss  6498  frecrdg  6679  oawordriexmid  6743  mapxpen  7148  findcard  7192  findcard2  7193  findcard2s  7194  ltapig  7705  ltanqi  7769  ltmnqi  7770  lt2addnq  7771  lt2mulnq  7772  prarloclemcalc  7869  genpassl  7891  genpassu  7892  prmuloc  7933  ltexprlemm  7967  ltexprlemfl  7976  ltexprlemfu  7978  lteupri  7984  ltaprg  7986  mul4  8459  add4  8488  cnegexlem2  8503  cnegexlem3  8504  2addsub  8541  addsubeq4  8542  muladd  8712  ltleadd  8775  reapmul1  8925  apreim  8933  receuap  9001  p1le  9181  lemul12b  9193  lbinf  9280  zdiv  9738  fzind  9765  fnn0ind  9766  uzss  9952  qmulcl  10046  qreccl  10051  xrlttr  10207  xaddass  10281  icc0r  10338  iooshf  10364  elfz5  10430  elfz0fzfz0  10543  fzind2  10668  ioo0  10704  ico0  10706  ioc0  10707  expnegap0  10997  expineg2  10998  mulexpzap  11029  expsubap  11037  expnbnd  11114  facndiv  11191  bccmpl  11206  bcval5  11215  bcpasc  11218  ccatrn  11391  swrdspsleq  11453  swrdccat2  11457  ccatpfx  11487  pfxccat1  11488  swrdswrd  11491  cats1un  11507  crim  11637  climshftlemg  12084  2sumeq2dv  12153  hash2iun  12262  2cprodeq2dv  12351  dvdsval3  12574  dvdsnegb  12591  muldvds1  12599  muldvds2  12600  dvdscmul  12601  dvdsmulc  12602  dvds2ln  12607  divalgb  12708  ndvdssub  12713  gcddiv  12812  rpexp1i  12949  phiprmpw  13020  hashgcdeq  13038  pythagtriplem1  13064  pockthg  13156  infpnlem1  13158  4sqlem3  13189  imasaddfnlemg  13684  mndpfo  13800  grplmulf1o  13928  grplactcnv  13956  mulgnn0subcl  13987  mulgsubcl  13988  mulgdir  14006  issubg2m  14041  issubgrpd2  14042  nmzsubg  14062  eqgen  14079  ghmmulg  14108  ghmf1  14125  kerf1ghm  14126  conjghm  14128  srglmhm  14346  srgrmhm  14347  ringlghm  14415  ringrghm  14416  oppr1g  14437  dvdsrcl2  14455  crngunit  14467  subsubrng  14571  subrgugrp  14597  subsubrg  14602  islmod  14676  lmodvsdir  14698  lmodvsass  14699  lsssubg  14763  lss1d  14769  lidlsubg  14872  lidlsubcl  14873  expghmap  14991  mulgghm2  14992  innei  15313  iscnp4  15368  cnpnei  15369  cnnei  15382  cnconst  15384  ismeti  15496  isxmet2d  15498  elbl2ps  15542  elbl2  15543  xblpnfps  15548  xblpnf  15549  xblm  15567  blininf  15574  blssexps  15579  blssex  15580  blsscls2  15643  metss  15644  metrest  15656  metcn  15664  divcnap  15715  cdivcncfap  15754  dvply1  15915  logdivlt  16046  lgslem4  16220  lgscllem  16224  lgsneg1  16242  lgsne0  16255  uspgr2wlkeq  16704  eupth2lem3lem7fi  16813