Theorem exp32 419

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 411	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	expd 414	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  exp44  436  exp45  437  expr  455  anassrs  466  an13s  649  3impb  1112  wereu  5678  f0rn0  6787  funfvima3  7254  isomin  7351  isoini  7352  ovg  7592  elovmpt3rab1  7687  onint  7799  peano5  7905  peano5OLD  7906  poseq  8169  tfrlem11  8415  tz7.48lem  8468  oalimcl  8587  oaass  8588  resixpfo  8961  fundmen  9062  ssfiALT  9205  php3  9243  php3OLD  9255  fodomfi  9357  marypha1lem  9464  card2inf  9586  ixpiunwdom  9621  cantnflt  9703  cnfcom  9731  dfac3  10152  dfac5lem5  10158  dfac5  10159  cfcoflem  10303  fin1a2s  10445  zorn2lem4  10530  zorn2lem7  10533  fpwwe2lem11  10672  wunfi  10752  grur1a  10850  addcanpi  10930  mulcanpi  10931  distrlem1pr  11056  ltaddpr  11065  ltexprlem1  11067  ltexprlem6  11072  ltexprlem7  11073  prodgt0  12099  mulgt1  12111  uzwo  12933  xmulasslem  13304  xlemul1a  13307  faclbnd  14289  swrdwrdsymb  14652  pfxccatin12lem2a  14717  pfxccat3  14724  swrdccat  14725  cshwidxmod  14793  s3iunsndisj  14955  dvdsaddre2b  16291  divgcdcoprm0  16643  cncongr2  16646  infpnlem1  16886  isacs4lem  18543  cycsubm  19164  gsmsymgrfixlem1  19389  gsmsymgrfix  19390  imasabl  19838  dmdprdsplit2lem  20009  pgpfac1  20044  pgpfac  20048  lssssr  20845  islmhm2  20930  lspdisj  21020  pzriprnglem5  21418  pzriprnglem8  21421  cygznlem2a  21508  lindfmm  21768  scmataddcl  22438  scmatsubcl  22439  scmatmulcl  22440  cpmatacl  22638  cayhamlem3  22809  cayleyhamilton1  22814  neindisj  23041  cnpnei  23188  t0dist  23249  ordthauslem  23307  uncmp  23327  fiuncmp  23328  iunconnlem  23351  fbasrn  23808  rnelfmlem  23876  rnelfm  23877  fmfnfmlem2  23879  fmfnfmlem4  23881  fclscf  23949  alexsubALTlem3  23973  alexsubALTlem4  23974  alexsubALT  23975  reconn  24764  fsumcn  24808  ovolfiniun  25450  dyadmax  25547  dyadmbllem  25548  dvmptfsum  25927  dvlip2  25948  dvivthlem1  25961  dvcnvrelem1  25970  ply1divex  26092  fta1g  26124  plydivex  26252  fta1  26263  mulcxp  26639  zabsle1  27249  lgsquad2lem2  27338  2lgsoddprm  27369  pntlem3  27562  nodenselem8  27644  nocvxmin  27731  precsexlem11  28135  om2noseqrdg  28197  brbtwn  28730  brcgr  28731  brbtwn2  28736  axeuclid  28794  finsumvtxdg2size  29384  uhgrwkspthlem2  29588  crctcshwlkn0  29652  wwlksnred  29723  wwlksnextinj  29730  umgr2wlk  29780  elwwlks2  29797  clwlkclwwlklem2a  29828  clwlkclwwlkf1lem3  29836  eupth2lems  30068  numclwwlk2lem1lem  30172  frgrregord013  30225  grpoidinvlem3  30336  shorth  31125  pjhthmo  31132  pjpjpre  31249  elspansn5  31404  lnopmi  31830  adjlnop  31916  leopmul2i  31965  stlesi  32071  ssmd2  32142  dmdsl3  32145  mdexchi  32165  cvexchlem  32198  atcv1  32210  atcvatlem  32215  atabsi  32231  mdsymlem2  32234  mdsymlem5  32237  sumdmdii  32245  sumdmdlem  32248  sumdmdlem2  32249  dya2iocnrect  33934  bnj571  34570  pconnconn  34874  iccllysconn  34893  satffunlem2lem1  35047  cgrextend  35637  btwnexch2  35652  colineardim1  35690  lineext  35705  btwnconn1lem13  35728  btwnconn1lem14  35729  seglecgr12im  35739  outsideofeq  35759  outsideofeu  35760  nn0prpwlem  35839  neibastop2lem  35877  tailfb  35894  nndivsub  35974  ee7.2aOLD  35978  fvineqsneu  36923  poimirlem31  37157  heicant  37161  filbcmb  37246  prdsbnd2  37301  heibor  37327  rngoisocnv  37487  ax12eq  38445  ax12el  38446  pmodlem2  39352  cdleme22b  39846  cdleme32d  39949  cdleme32f  39951  trlord  40074  cdlemj2  40327  cdlemk38  40420  cdlemk19x  40448  dihord2pre  40730  fsuppind  41854  mzpcompact2lem  42202  pellfundex  42337  acongsym  42428  pwssplit4  42544  pwslnm  42549  cantnfresb  42784  relexpmulg  43171  stoweidlem17  45434  2reu8i  46522  imasetpreimafvbijlemf1  46773  iccpartigtl  46792  paireqne  46880  fmtnofac2lem  46937  2pwp1prmfmtno  46959  lighneallem4  46979  bgoldbtbndlem2  47175  bgoldbtbndlem3  47176  bgoldbtbnd  47178  isuspgrimlem  47250  grimco  47256  lmod0rng  47369  2zrngamgm  47385