Theorem exp32 420

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

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

Assertion

Ref	Expression
exp32	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem exp32

Step	Hyp	Ref	Expression
1		exp32.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	ex 412	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	expd 415	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  exp44  437  exp45  438  expr  456  anassrs  467  an13s  651  3impb  1114  wereu  5619  f0rn0  6713  funfvima3  7176  dff14i  7200  isomin  7278  isoini  7279  ovg  7518  elovmpt3rab1  7613  onint  7730  peano5  7833  poseq  8098  tfrlem11  8317  tz7.48lem  8370  oalimcl  8485  oaass  8486  resixpfo  8870  fundmen  8963  ssfiALT  9098  php3  9133  fodomfi  9219  fodomfiOLD  9239  marypha1lem  9342  card2inf  9466  ixpiunwdom  9501  cantnflt  9587  cnfcom  9615  dfac3  10034  dfac5lem5  10040  dfac5  10042  cfcoflem  10185  fin1a2s  10327  zorn2lem4  10412  zorn2lem7  10415  fpwwe2lem11  10554  wunfi  10634  grur1a  10732  addcanpi  10812  mulcanpi  10813  distrlem1pr  10938  ltaddpr  10947  ltexprlem1  10949  ltexprlem6  10954  ltexprlem7  10955  prodgt0  11989  mulgt1OLD  12001  uzwo  12830  xmulasslem  13205  xlemul1a  13208  faclbnd  14215  swrdwrdsymb  14587  pfxccatin12lem2a  14651  pfxccat3  14658  swrdccat  14659  cshwidxmod  14727  s3iunsndisj  14893  dvdsaddre2b  16236  divgcdcoprm0  16594  cncongr2  16597  infpnlem1  16840  isacs4lem  18468  cycsubm  19099  gsmsymgrfixlem1  19324  gsmsymgrfix  19325  imasabl  19773  dmdprdsplit2lem  19944  pgpfac1  19979  pgpfac  19983  lssssr  20875  islmhm2  20960  lspdisj  21050  pzriprnglem5  21410  pzriprnglem8  21413  cygznlem2a  21492  lindfmm  21752  scmataddcl  22419  scmatsubcl  22420  scmatmulcl  22421  cpmatacl  22619  cayhamlem3  22790  cayleyhamilton1  22795  neindisj  23020  cnpnei  23167  t0dist  23228  ordthauslem  23286  uncmp  23306  fiuncmp  23307  iunconnlem  23330  fbasrn  23787  rnelfmlem  23855  rnelfm  23856  fmfnfmlem2  23858  fmfnfmlem4  23860  fclscf  23928  alexsubALTlem3  23952  alexsubALTlem4  23953  alexsubALT  23954  reconn  24733  fsumcn  24777  ovolfiniun  25418  dyadmax  25515  dyadmbllem  25516  dvmptfsum  25895  dvlip2  25916  dvivthlem1  25929  dvcnvrelem1  25938  ply1divex  26058  fta1g  26091  plydivex  26221  fta1  26232  mulcxp  26610  zabsle1  27223  lgsquad2lem2  27312  2lgsoddprm  27343  pntlem3  27536  nodenselem8  27619  nocvxmin  27707  precsexlem11  28142  om2noseqrdg  28221  expadds  28345  brbtwn  28862  brcgr  28863  brbtwn2  28868  axeuclid  28926  finsumvtxdg2size  29514  uhgrwkspthlem2  29717  crctcshwlkn0  29784  wwlksnred  29855  wwlksnextinj  29862  umgr2wlk  29912  elwwlks2  29929  clwlkclwwlklem2a  29960  clwlkclwwlkf1lem3  29968  eupth2lems  30200  numclwwlk2lem1lem  30304  frgrregord013  30357  grpoidinvlem3  30468  shorth  31257  pjhthmo  31264  pjpjpre  31381  elspansn5  31536  lnopmi  31962  adjlnop  32048  leopmul2i  32097  stlesi  32203  ssmd2  32274  dmdsl3  32277  mdexchi  32297  cvexchlem  32330  atcv1  32342  atcvatlem  32347  atabsi  32363  mdsymlem2  32366  mdsymlem5  32369  sumdmdii  32377  sumdmdlem  32380  sumdmdlem2  32381  dya2iocnrect  34248  bnj571  34872  pconnconn  35203  iccllysconn  35222  satffunlem2lem1  35376  cgrextend  35981  btwnexch2  35996  colineardim1  36034  lineext  36049  btwnconn1lem13  36072  btwnconn1lem14  36073  seglecgr12im  36083  outsideofeq  36103  outsideofeu  36104  nn0prpwlem  36295  neibastop2lem  36333  tailfb  36350  nndivsub  36430  ee7.2aOLD  36434  fvineqsneu  37384  poimirlem31  37630  heicant  37634  filbcmb  37719  prdsbnd2  37774  heibor  37800  rngoisocnv  37960  ax12eq  38919  ax12el  38920  pmodlem2  39826  cdleme22b  40320  cdleme32d  40423  cdleme32f  40425  trlord  40548  cdlemj2  40801  cdlemk38  40894  cdlemk19x  40922  dihord2pre  41204  fsuppind  42563  mzpcompact2lem  42724  pellfundex  42859  acongsym  42949  pwssplit4  43062  pwslnm  43067  cantnfresb  43297  relexpmulg  43683  relpmin  44926  stoweidlem17  45999  2reu8i  47098  imasetpreimafvbijlemf1  47389  iccpartigtl  47408  paireqne  47496  fmtnofac2lem  47553  2pwp1prmfmtno  47575  lighneallem4  47595  bgoldbtbndlem2  47791  bgoldbtbndlem3  47792  bgoldbtbnd  47794  grimco  47874  isuspgrimlem  47880  cycl3grtri  47932  isubgr3stgrlem6  47956  lmod0rng  48214  2zrngamgm  48230