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  3145  rabssdv  4050  reupick2  4306  disjiund  5110  otiunsndisj  5495  wefrc  5648  tz7.7  6378  unizlim  6476  funimassd  6944  fvelimad  6945  fveqdmss  7067  fompt  7107  f1oiso2  7344  ssorduni  7771  sucexeloniOLD  7802  suceloniOLD  7804  tfisi  7852  resf1extb  7928  funeldmdif  8045  poxp  8125  poseq  8155  fpr3g  8282  frrlem10  8292  smo11  8376  tfrlem5  8392  odi  8589  omass  8590  nndi  8633  nnmass  8634  naddoa  8712  undifixp  8946  findcard  9175  php3  9221  ac6sfi  9290  domunfican  9331  mapfien2  9419  fisup2g  9479  fiinf2g  9512  ttrclss  9732  ttrclselem2  9738  indcardi  10053  acndom  10063  ackbij1lem16  10246  infpssrlem4  10318  fin23lem11  10329  isfin2-2  10331  fin23lem34  10358  fin1a2lem10  10421  hsmexlem2  10439  axcc3  10450  domtriomlem  10454  axdc3lem2  10463  axdc3lem4  10465  axcclem  10469  ttukeyg  10529  axdclem2  10532  axacndlem4  10622  axacndlem5  10623  axacnd  10624  tskr1om2  10780  tskwe2  10785  tskord  10792  tskcard  10793  tskuni  10795  tskwun  10796  gruiin  10822  grudomon  10829  gruina  10830  mulcanpi  10912  adderpq  10968  mulerpq  10969  dedekindle  11397  divgt0  12108  divge0  12109  nnne0  12272  uzind  12683  uzind2  12684  iccsplit  13500  ssnn0fi  14001  expmordi  14183  sqlecan  14225  modexp  14254  expnngt1  14257  facavg  14317  2cshwcshw  14842  relexpcnv  15052  relexpaddnn  15068  relexpaddg  15070  pwdif  15882  prodfn0  15908  prodfrec  15909  ntrivcvgfvn0  15913  fprodabs  15988  bpolycl  16066  bpolydif  16069  fprodefsum  16109  dvdsmodexp  16278  dvdsaddre2b  16324  nn0rppwr  16578  dvdsnprmd  16707  2mulprm  16710  prmndvdsfaclt  16742  ncoprmlnprm  16745  fermltl  16801  pceu  16864  setsstruct2  17191  setsstruct  17193  mreexexd  17658  isglbd  18517  symgpssefmnd  19375  pmtrfrn  19437  psgnunilem4  19476  ablsimpgprmd  20096  mulgass2  20267  islss4  20917  lspsneu  21082  lspfixed  21087  lspexch  21088  lsmcv  21100  lspsolvlem  21101  rnglidlmcl  21175  xrsdsreclblem  21378  nzerooringczr  21439  isphld  21612  mdetralt  22544  mdetunilem9  22556  fiinopn  22837  neips  23049  tpnei  23057  neindisj2  23059  opnneiid  23062  hausnei2  23289  cmpsublem  23335  cmpsub  23336  cmpcld  23338  comppfsc  23468  filufint  23856  cfinufil  23864  rnelfm  23889  alexsubALTlem1  23983  alexsubALTlem4  23986  alexsubALT  23987  tsmsxp  24091  neibl  24438  tngngp3  24593  tgqioo  24737  ovolunlem2  25449  iunmbl2  25508  itg1le  25664  vieta1  26270  aannenlem2  26287  aalioulem3  26292  aalioulem4  26293  aaliou2  26298  wilthlem3  27030  bcmono  27238  gausslemma2dlem1a  27326  sslttr  27769  ssltun1  27770  ssltun2  27771  sltlpss  27862  precsexlem8  28155  precsexlem9  28156  precsex  28159  expscl  28330  expsgt0  28332  pw2cut  28337  iscgrglt  28439  axcontlem7  28895  elntg2  28910  edglnl  29068  numedglnl  29069  ausgrumgri  29092  ausgrusgri  29093  usgrausgrb  29094  usgredg2vtxeuALT  29147  ushgredgedg  29154  ushgredgedgloop  29156  nbuhgr2vtx1edgb  29277  cusgrsize2inds  29379  upgrewlkle2  29532  wlkl1loop  29564  redwlk  29598  pthdivtx  29655  pthdadjvtx  29656  upgr2pthnlp  29660  upgrspthswlk  29666  clwlkl1loop  29711  cyclnumvtx  29728  wwlksnred  29820  wwlksnextbi  29822  elwwlks2ons3im  29882  umgrwwlks2on  29885  clwwlknwwlksn  29965  clwwlkinwwlk  29967  wwlksext2clwwlk  29984  1pthon2v  30080  uhgr3cyclex  30109  n4cyclfrgr  30218  frgrwopreg  30250  numclwwlk1lem2f1  30284  clwwlknonclwlknonf1o  30289  wlkl0  30294  frgrreggt1  30320  frgrreg  30321  frgrregord013  30322  chintcli  31258  spansnss  31498  elspansn4  31500  chscllem4  31567  hoadddir  31731  adjmul  32019  kbass6  32048  spansncv2  32220  sumdmdii  32342  nexple  32769  bnj1417  35018  lfuhgr2  35087  cusgredgex  35090  sat1el2xp  35347  fmlasuc  35354  satffunlem1lem1  35370  satffunlem2lem1  35372  mclsind  35538  iprodefisumlem  35703  btwndiff  35991  elicc3  36281  finminlem  36282  sdclem2  37712  clmgmOLD  37821  grpomndo  37845  zerdivemp1x  37917  lsmsat  38972  lsmcv2  38993  lcvat  38994  lsatcveq0  38996  lcvexchlem4  39001  lcvexchlem5  39002  islshpcv  39017  l1cvpat  39018  lshpkrlem6  39079  omlfh3N  39223  cvlsupr4  39309  cvlsupr5  39310  cvlsupr6  39311  2llnneN  39374  hlrelat3  39377  cvrval3  39378  cvrval4N  39379  cvrexchlem  39384  2atlt  39404  cvrat4  39408  atbtwnexOLDN  39412  atbtwnex  39413  athgt  39421  3dim1  39432  3dim2  39433  3dim3  39434  1cvratex  39438  llnle  39483  atcvrlln2  39484  atcvrlln  39485  2llnmat  39489  lplnle  39505  lplnnle2at  39506  lplnnlelln  39508  llncvrlpln2  39522  2llnjN  39532  lvoli2  39546  lvolnlelln  39549  lvolnlelpln  39550  4atlem10  39571  4atlem11  39574  4atlem12  39577  lplncvrlvol2  39580  2lplnj  39585  lneq2at  39743  lnatexN  39744  lnjatN  39745  lncvrat  39747  2lnat  39749  cdlemb  39759  paddasslem14  39798  llnexchb2  39834  dalawlem10  39845  dalawlem13  39848  dalawlem14  39849  dalaw  39851  pclclN  39856  pclfinN  39865  osumcllem11N  39931  lhp2lt  39966  lhpexle3lem  39976  4atexlem7  40040  ldilcnv  40080  ldilco  40081  ltrncnv  40111  trlval2  40128  cdleme24  40317  cdleme26ee  40325  cdleme28  40338  cdleme32le  40412  cdleme50trn2  40516  cdleme50ltrn  40522  cdleme  40525  cdlemf1  40526  cdlemf  40528  cdlemg1cex  40553  cdlemg2ce  40557  cdlemg18b  40644  ltrnco  40684  tendocan  40789  cdlemk28-3  40873  cdlemk11t  40911  dia2dimlem6  41034  dia2dimlem12  41040  dihlsscpre  41199  dihord4  41223  dihord5b  41224  dihmeetlem3N  41270  dihmeetlem20N  41291  dvh4dimlem  41408  lclkrlem2y  41496  mapdpglem24  41669  mapdpglem32  41670  mapdpg  41671  baerlem3lem2  41675  baerlem5alem2  41676  baerlem5blem2  41677  mapdh9a  41754  mapdh9aOLDN  41755  hdmap14lem6  41838  hdmapglem7  41894  indstrd  42152  nnadddir  42267  nnmulcom  42269  sn-addlid  42394  remulcand  42428  mzpexpmpt  42715  pellexlem5  42803  pellex  42805  pell14qrexpclnn0  42836  pellfundex  42856  monotuz  42912  monotoddzzfi  42913  rmxypos  42918  jm2.17a  42931  jm2.17b  42932  rmygeid  42935  jm2.19lem3  42962  jm2.15nn0  42974  jm2.16nn0  42975  aomclem2  43026  aomclem6  43030  dfac11  43033  hbtlem5  43099  cnsrexpcl  43136  cantnf2  43296  dflim5  43300  relexpxpnnidm  43674  relexpiidm  43675  relexpss1d  43676  iunrelexpmin1  43679  relexpmulnn  43680  iunrelexpmin2  43683  relexp01min  43684  relexp0a  43687  relexpxpmin  43688  relexpaddss  43689  trclimalb2  43697  tfindsd  44182  3impexpbicomi  44454  ee333  44480  eel12131  44685  eel2122old  44690  e333  44705  ordelordALTVD  44839  refsumcn  45002  uzwo4  45025  ssinc  45059  ssdec  45060  iunincfi  45066  restuni3  45090  eliuniin2  45092  rabssd  45114  reximdd  45120  suprnmpt  45146  disjf1o  45163  disjinfi  45164  ssnnf1octb  45166  choicefi  45172  mapssbi  45185  unirnmapsn  45186  iunmapsn  45189  rnmptlb  45215  rnmptbddlem  45216  infnsuprnmpt  45222  fperiodmullem  45280  upbdrech  45282  ssfiunibd  45286  supxrgere  45308  iuneqfzuzlem  45309  supxrgelem  45312  supxrge  45313  suplesup  45314  infrpge  45326  infleinf  45347  suplesup2  45351  supxrunb3  45374  infleinf2  45389  rexabslelem  45393  infrnmptle  45398  infxrunb3rnmpt  45403  iccshift  45495  iooshift  45499  fmul01  45557  fmuldfeq  45560  fmul01lt1  45563  mullimc  45593  islptre  45596  mullimcf  45600  limcperiod  45605  islpcn  45616  limsupre  45618  limcleqr  45621  neglimc  45624  addlimc  45625  0ellimcdiv  45626  limclner  45628  fnlimfvre  45651  limsuppnflem  45687  limsupmnfuzlem  45703  limsupre3lem  45709  limsupre3uzlem  45712  climuzlem  45720  limsupgtlem  45754  coskpi2  45843  cosknegpi  45846  cncfshift  45851  cncfperiod  45856  icccncfext  45864  dvnmptdivc  45915  dvnmptconst  45918  dvnmul  45920  dvmptfprodlem  45921  dvmptfprod  45922  dvnprodlem1  45923  dvnprodlem2  45924  iblspltprt  45950  itgspltprt  45956  itgperiod  45958  ismbl3  45963  stoweidlem3  45980  stoweidlem31  46008  stoweidlem59  46036  stirlinglem13  46063  fourierdlem41  46125  fourierdlem42  46126  fourierdlem48  46131  fourierdlem51  46134  fourierdlem70  46153  fourierdlem71  46154  fourierdlem73  46156  fourierdlem80  46163  fourierdlem81  46164  fourierdlem89  46172  fourierdlem91  46174  fourierdlem93  46176  fourierdlem97  46180  elaa2  46211  qndenserrnopnlem  46274  salexct  46311  subsaliuncl  46335  subsalsal  46336  sge0tsms  46357  sge0f1o  46359  sge0fsum  46364  sge0supre  46366  sge0sup  46368  sge0rnbnd  46370  sge0gerp  46372  sge0pnffigt  46373  sge0lefi  46375  sge0ltfirp  46377  sge0resrn  46381  sge0resplit  46383  sge0split  46386  sge0iunmptlemfi  46390  sge0iunmptlemre  46392  sge0iunmpt  46395  sge0rpcpnf  46398  sge0isum  46404  sge0xp  46406  sge0xaddlem2  46411  sge0uzfsumgt  46421  sge0seq  46423  sge0reuz  46424  nnfoctbdjlem  46432  nnfoctbdj  46433  iundjiun  46437  meadjiunlem  46442  voliunsge0lem  46449  meaiuninclem  46457  meaiininc2  46465  carageniuncllem1  46498  carageniuncllem2  46499  caratheodorylem1  46503  caratheodorylem2  46504  isomenndlem  46507  ovnsupge0  46534  ovnlerp  46539  ovncvrrp  46541  ovnsubaddlem1  46547  hoidmvval0  46564  hoidmv1lelem3  46570  hoidmv1le  46571  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem3  46574  ovnhoilem2  46579  opnvonmbllem2  46610  ovnovollem3  46635  vonioo  46659  vonicc  46662  pimiooltgt  46687  sssmf  46715  smfaddlem1  46740  smflimlem6  46753  smfmullem4  46771  smfpimbor1lem1  46775  smfco  46779  smfpimcc  46785  smflimmpt  46787  smfinflem  46794  smflimsuplem7  46803  smflimsuplem8  46804  smflimsupmpt  46806  smfliminfmpt  46809  cfsetsnfsetf1  47036  2tceilhalfelfzo1  47309  elsetpreimafveqfv  47354  iccpartiltu  47384  sprsymrelfvlem  47452  reuopreuprim  47488  goldbachth  47509  fmtnofac1  47532  prmdvdsfmtnof1lem1  47546  lighneal  47573  grimuhgr  47848  uhgrimedgi  47851  uhgrimisgrgriclem  47891  clnbgrgrim  47895  grimedg  47896  usgrgrtrirex  47910  isubgr3stgrlem3  47928  isubgr3stgrlem6  47931  uspgrlimlem2  47949  grlimgrtri  47956  grlicsym  47966  clnbgr3stgrgrlic  47972  gpgusgralem  48008  gpgedgvtx1  48014  gpgvtxedg0  48015  gpgvtxedg1  48016  uspgropssxp  48067  rngccatidALTV  48195  ringccatidALTV  48229  lcosslsp  48362  fllog2  48496  dignn0flhalf  48546  fv1arycl  48565  1arymaptf1  48570  fv2arycl  48576  2arymaptf1  48581  itschlc0yqe  48688  itsclc0xyqsol  48696  seposep  48848  iscnrm3lem6  48860  iunord  49488  setrec2fun  49504