Theorem 3exp 1119

Description: Exportation inference. (Contributed by NM, 30-May-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)

Hypothesis

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

Assertion

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

Proof of Theorem 3exp

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expa 1118	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	exp31 419	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ w3a 1086

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  df-3an 1088

This theorem is referenced by:  3expb  1120  3expib  1122  3com12  1123  3com13  1124  pm3.2an3  1341  3exp1  1353  3expd  1354  exp5o  1356  3ecase  1476  rexlimdv3a  3138  rabssdv  4034  reupick2  4290  disjiund  5093  otiunsndisj  5475  wefrc  5625  tz7.7  6346  unizlim  6445  funimassd  6909  fvelimad  6910  fveqdmss  7032  fompt  7072  f1oiso2  7309  ssorduni  7735  sucexeloniOLD  7766  tfisi  7815  resf1extb  7890  funeldmdif  8006  poxp  8084  poseq  8114  fpr3g  8241  frrlem10  8251  smo11  8310  tfrlem5  8325  odi  8520  omass  8521  nndi  8564  nnmass  8565  naddoa  8643  undifixp  8884  findcard  9104  php3  9150  ac6sfi  9207  domunfican  9248  mapfien2  9336  fisup2g  9396  fiinf2g  9429  ttrclss  9649  ttrclselem2  9655  indcardi  9970  acndom  9980  ackbij1lem16  10163  infpssrlem4  10235  fin23lem11  10246  isfin2-2  10248  fin23lem34  10275  fin1a2lem10  10338  hsmexlem2  10356  axcc3  10367  domtriomlem  10371  axdc3lem2  10380  axdc3lem4  10382  axcclem  10386  ttukeyg  10446  axdclem2  10449  axacndlem4  10539  axacndlem5  10540  axacnd  10541  tskr1om2  10697  tskwe2  10702  tskord  10709  tskcard  10710  tskuni  10712  tskwun  10713  gruiin  10739  grudomon  10746  gruina  10747  mulcanpi  10829  adderpq  10885  mulerpq  10886  dedekindle  11314  divgt0  12027  divge0  12028  nnne0  12196  uzind  12602  uzind2  12603  iccsplit  13422  ssnn0fi  13926  expmordi  14108  sqlecan  14150  modexp  14179  expnngt1  14182  facavg  14242  2cshwcshw  14767  relexpcnv  14977  relexpaddnn  14993  relexpaddg  14995  pwdif  15810  prodfn0  15836  prodfrec  15837  ntrivcvgfvn0  15841  fprodabs  15916  bpolycl  15994  bpolydif  15997  fprodefsum  16037  dvdsmodexp  16206  dvdsaddre2b  16253  nn0rppwr  16507  dvdsnprmd  16636  2mulprm  16639  prmndvdsfaclt  16671  ncoprmlnprm  16674  fermltl  16730  pceu  16793  setsstruct2  17120  setsstruct  17122  mreexexd  17585  isglbd  18444  symgpssefmnd  19302  pmtrfrn  19364  psgnunilem4  19403  ablsimpgprmd  20023  mulgass2  20194  islss4  20844  lspsneu  21009  lspfixed  21014  lspexch  21015  lsmcv  21027  lspsolvlem  21028  rnglidlmcl  21102  xrsdsreclblem  21305  nzerooringczr  21366  isphld  21539  mdetralt  22471  mdetunilem9  22483  fiinopn  22764  neips  22976  tpnei  22984  neindisj2  22986  opnneiid  22989  hausnei2  23216  cmpsublem  23262  cmpsub  23263  cmpcld  23265  comppfsc  23395  filufint  23783  cfinufil  23791  rnelfm  23816  alexsubALTlem1  23910  alexsubALTlem4  23913  alexsubALT  23914  tsmsxp  24018  neibl  24365  tngngp3  24520  tgqioo  24664  ovolunlem2  25375  iunmbl2  25434  itg1le  25590  vieta1  26196  aannenlem2  26213  aalioulem3  26218  aalioulem4  26219  aaliou2  26224  wilthlem3  26956  bcmono  27164  gausslemma2dlem1a  27252  sslttr  27695  ssltun1  27696  ssltun2  27697  sltlpss  27795  precsexlem8  28092  precsexlem9  28093  precsex  28096  onsfi  28223  expscllem  28292  expsgt0  28298  pw2cut  28311  iscgrglt  28417  axcontlem7  28873  elntg2  28888  edglnl  29046  numedglnl  29047  ausgrumgri  29070  ausgrusgri  29071  usgrausgrb  29072  usgredg2vtxeuALT  29125  ushgredgedg  29132  ushgredgedgloop  29134  nbuhgr2vtx1edgb  29255  cusgrsize2inds  29357  upgrewlkle2  29510  wlkl1loop  29541  redwlk  29574  pthdivtx  29630  pthdadjvtx  29631  upgr2pthnlp  29635  upgrspthswlk  29641  clwlkl1loop  29686  cyclnumvtx  29703  wwlksnred  29795  wwlksnextbi  29797  elwwlks2ons3im  29857  umgrwwlks2on  29860  clwwlknwwlksn  29940  clwwlkinwwlk  29942  wwlksext2clwwlk  29959  1pthon2v  30055  uhgr3cyclex  30084  n4cyclfrgr  30193  frgrwopreg  30225  numclwwlk1lem2f1  30259  clwwlknonclwlknonf1o  30264  wlkl0  30269  frgrreggt1  30295  frgrreg  30296  frgrregord013  30297  chintcli  31233  spansnss  31473  elspansn4  31475  chscllem4  31542  hoadddir  31706  adjmul  31994  kbass6  32023  spansncv2  32195  sumdmdii  32317  nexple  32742  bnj1417  35004  lfuhgr2  35079  cusgredgex  35082  sat1el2xp  35339  fmlasuc  35346  satffunlem1lem1  35362  satffunlem2lem1  35364  mclsind  35530  iprodefisumlem  35700  btwndiff  35988  elicc3  36278  finminlem  36279  sdclem2  37709  clmgmOLD  37818  grpomndo  37842  zerdivemp1x  37914  lsmsat  38974  lsmcv2  38995  lcvat  38996  lsatcveq0  38998  lcvexchlem4  39003  lcvexchlem5  39004  islshpcv  39019  l1cvpat  39020  lshpkrlem6  39081  omlfh3N  39225  cvlsupr4  39311  cvlsupr5  39312  cvlsupr6  39313  2llnneN  39376  hlrelat3  39379  cvrval3  39380  cvrval4N  39381  cvrexchlem  39386  2atlt  39406  cvrat4  39410  atbtwnexOLDN  39414  atbtwnex  39415  athgt  39423  3dim1  39434  3dim2  39435  3dim3  39436  1cvratex  39440  llnle  39485  atcvrlln2  39486  atcvrlln  39487  2llnmat  39491  lplnle  39507  lplnnle2at  39508  lplnnlelln  39510  llncvrlpln2  39524  2llnjN  39534  lvoli2  39548  lvolnlelln  39551  lvolnlelpln  39552  4atlem10  39573  4atlem11  39576  4atlem12  39579  lplncvrlvol2  39582  2lplnj  39587  lneq2at  39745  lnatexN  39746  lnjatN  39747  lncvrat  39749  2lnat  39751  cdlemb  39761  paddasslem14  39800  llnexchb2  39836  dalawlem10  39847  dalawlem13  39850  dalawlem14  39851  dalaw  39853  pclclN  39858  pclfinN  39867  osumcllem11N  39933  lhp2lt  39968  lhpexle3lem  39978  4atexlem7  40042  ldilcnv  40082  ldilco  40083  ltrncnv  40113  trlval2  40130  cdleme24  40319  cdleme26ee  40327  cdleme28  40340  cdleme32le  40414  cdleme50trn2  40518  cdleme50ltrn  40524  cdleme  40527  cdlemf1  40528  cdlemf  40530  cdlemg1cex  40555  cdlemg2ce  40559  cdlemg18b  40646  ltrnco  40686  tendocan  40791  cdlemk28-3  40875  cdlemk11t  40913  dia2dimlem6  41036  dia2dimlem12  41042  dihlsscpre  41201  dihord4  41225  dihord5b  41226  dihmeetlem3N  41272  dihmeetlem20N  41293  dvh4dimlem  41410  lclkrlem2y  41498  mapdpglem24  41671  mapdpglem32  41672  mapdpg  41673  baerlem3lem2  41677  baerlem5alem2  41678  baerlem5blem2  41679  mapdh9a  41756  mapdh9aOLDN  41757  hdmap14lem6  41840  hdmapglem7  41896  indstrd  42154  nnadddir  42231  nnmulcom  42233  sn-addlid  42365  remulcand  42400  mzpexpmpt  42706  pellexlem5  42794  pellex  42796  pell14qrexpclnn0  42827  pellfundex  42847  monotuz  42903  monotoddzzfi  42904  rmxypos  42909  jm2.17a  42922  jm2.17b  42923  rmygeid  42926  jm2.19lem3  42953  jm2.15nn0  42965  jm2.16nn0  42966  aomclem2  43017  aomclem6  43021  dfac11  43024  hbtlem5  43090  cnsrexpcl  43127  cantnf2  43287  dflim5  43291  relexpxpnnidm  43665  relexpiidm  43666  relexpss1d  43667  iunrelexpmin1  43670  relexpmulnn  43671  iunrelexpmin2  43674  relexp01min  43675  relexp0a  43678  relexpxpmin  43679  relexpaddss  43680  trclimalb2  43688  tfindsd  44172  3impexpbicomi  44444  ee333  44470  eel12131  44675  eel2122old  44680  e333  44695  ordelordALTVD  44829  refsumcn  44997  uzwo4  45020  ssinc  45054  ssdec  45055  iunincfi  45061  restuni3  45085  eliuniin2  45087  rabssd  45109  reximdd  45115  suprnmpt  45141  disjf1o  45158  disjinfi  45159  ssnnf1octb  45161  choicefi  45167  mapssbi  45180  unirnmapsn  45181  iunmapsn  45184  rnmptlb  45210  rnmptbddlem  45211  infnsuprnmpt  45217  fperiodmullem  45274  upbdrech  45276  ssfiunibd  45280  supxrgere  45302  iuneqfzuzlem  45303  supxrgelem  45306  supxrge  45307  suplesup  45308  infrpge  45320  infleinf  45341  suplesup2  45345  supxrunb3  45368  infleinf2  45383  rexabslelem  45387  infrnmptle  45392  infxrunb3rnmpt  45397  iccshift  45489  iooshift  45493  fmul01  45551  fmuldfeq  45554  fmul01lt1  45557  mullimc  45587  islptre  45590  mullimcf  45594  limcperiod  45599  islpcn  45610  limsupre  45612  limcleqr  45615  neglimc  45618  addlimc  45619  0ellimcdiv  45620  limclner  45622  fnlimfvre  45645  limsuppnflem  45681  limsupmnfuzlem  45697  limsupre3lem  45703  limsupre3uzlem  45706  climuzlem  45714  limsupgtlem  45748  coskpi2  45837  cosknegpi  45840  cncfshift  45845  cncfperiod  45850  icccncfext  45858  dvnmptdivc  45909  dvnmptconst  45912  dvnmul  45914  dvmptfprodlem  45915  dvmptfprod  45916  dvnprodlem1  45917  dvnprodlem2  45918  iblspltprt  45944  itgspltprt  45950  itgperiod  45952  ismbl3  45957  stoweidlem3  45974  stoweidlem31  46002  stoweidlem59  46030  stirlinglem13  46057  fourierdlem41  46119  fourierdlem42  46120  fourierdlem48  46125  fourierdlem51  46128  fourierdlem70  46147  fourierdlem71  46148  fourierdlem73  46150  fourierdlem80  46157  fourierdlem81  46158  fourierdlem89  46166  fourierdlem91  46168  fourierdlem93  46170  fourierdlem97  46174  elaa2  46205  qndenserrnopnlem  46268  salexct  46305  subsaliuncl  46329  subsalsal  46330  sge0tsms  46351  sge0f1o  46353  sge0fsum  46358  sge0supre  46360  sge0sup  46362  sge0rnbnd  46364  sge0gerp  46366  sge0pnffigt  46367  sge0lefi  46369  sge0ltfirp  46371  sge0resrn  46375  sge0resplit  46377  sge0split  46380  sge0iunmptlemfi  46384  sge0iunmptlemre  46386  sge0iunmpt  46389  sge0rpcpnf  46392  sge0isum  46398  sge0xp  46400  sge0xaddlem2  46405  sge0uzfsumgt  46415  sge0seq  46417  sge0reuz  46418  nnfoctbdjlem  46426  nnfoctbdj  46427  iundjiun  46431  meadjiunlem  46436  voliunsge0lem  46443  meaiuninclem  46451  meaiininc2  46459  carageniuncllem1  46492  carageniuncllem2  46493  caratheodorylem1  46497  caratheodorylem2  46498  isomenndlem  46501  ovnsupge0  46528  ovnlerp  46533  ovncvrrp  46535  ovnsubaddlem1  46541  hoidmvval0  46558  hoidmv1lelem3  46564  hoidmv1le  46565  hoidmvlelem1  46566  hoidmvlelem2  46567  hoidmvlelem3  46568  ovnhoilem2  46573  opnvonmbllem2  46604  ovnovollem3  46629  vonioo  46653  vonicc  46656  pimiooltgt  46681  sssmf  46709  smfaddlem1  46734  smflimlem6  46747  smfmullem4  46765  smfpimbor1lem1  46769  smfco  46773  smfpimcc  46779  smflimmpt  46781  smfinflem  46788  smflimsuplem7  46797  smflimsuplem8  46798  smflimsupmpt  46800  smfliminfmpt  46803  cfsetsnfsetf1  47033  2tceilhalfelfzo1  47306  elsetpreimafveqfv  47366  iccpartiltu  47396  sprsymrelfvlem  47464  reuopreuprim  47500  goldbachth  47521  fmtnofac1  47544  prmdvdsfmtnof1lem1  47558  lighneal  47585  grimuhgr  47860  uhgrimedgi  47863  uhgrimisgrgriclem  47903  clnbgrgrim  47907  grimedg  47908  usgrgrtrirex  47922  isubgr3stgrlem3  47940  isubgr3stgrlem6  47943  uspgrlimlem2  47961  grlimgrtri  47968  grlicsym  47978  clnbgr3stgrgrlic  47984  gpgusgralem  48020  gpgedgvtx1  48026  gpgvtxedg0  48027  gpgvtxedg1  48028  uspgropssxp  48105  rngccatidALTV  48233  ringccatidALTV  48267  lcosslsp  48400  fllog2  48530  dignn0flhalf  48580  fv1arycl  48599  1arymaptf1  48604  fv2arycl  48610  2arymaptf1  48615  itschlc0yqe  48722  itsclc0xyqsol  48730  seposep  48887  iscnrm3lem6  48899  iunord  49638  setrec2fun  49654