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 420	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  3expb  1120  3expib  1122  3com12  1123  3com13  1124  pm3.2an3  1340  3exp1  1352  3expd  1353  exp5o  1355  3ecase  1474  rexlimdv3a  3159  rabssdv  4072  reupick2  4320  disjiund  5138  otiunsndisj  5520  wefrc  5670  tz7.7  6390  unizlim  6487  funimassd  6958  fvelimad  6959  fveqdmss  7080  f1oiso2  7348  ssorduni  7765  sucexeloniOLD  7797  suceloniOLD  7799  tfisi  7847  funeldmdif  8033  poxp  8113  poseq  8143  fpr3g  8269  frrlem10  8279  smo11  8363  tfrlem5  8379  odi  8578  omass  8579  nndi  8622  nnmass  8623  undifixp  8927  findcard  9162  php3  9211  ac6sfi  9286  domunfican  9319  mapfien2  9403  fisup2g  9462  fiinf2g  9494  ttrclss  9714  ttrclselem2  9720  indcardi  10035  acndom  10045  ackbij1lem16  10229  infpssrlem4  10300  fin23lem11  10311  isfin2-2  10313  fin23lem34  10340  fin1a2lem10  10403  hsmexlem2  10421  axcc3  10432  domtriomlem  10436  axdc3lem2  10445  axdc3lem4  10447  axcclem  10451  ttukeyg  10511  axdclem2  10514  axacndlem4  10604  axacndlem5  10605  axacnd  10606  tskr1om2  10762  tskwe2  10767  tskord  10774  tskcard  10775  tskuni  10777  tskwun  10778  gruiin  10804  grudomon  10811  gruina  10812  mulcanpi  10894  adderpq  10950  mulerpq  10951  dedekindle  11377  divgt0  12081  divge0  12082  nnne0  12245  uzind  12653  uzind2  12654  iccsplit  13461  ssnn0fi  13949  expmordi  14131  sqlecan  14172  modexp  14200  expnngt1  14203  facavg  14260  2cshwcshw  14775  relexpcnv  14981  relexpaddnn  14997  relexpaddg  14999  pwdif  15813  prodfn0  15839  prodfrec  15840  ntrivcvgfvn0  15844  fprodabs  15917  bpolycl  15995  bpolydif  15998  fprodefsum  16037  dvdsmodexp  16204  dvdsaddre2b  16249  dvdsnprmd  16626  2mulprm  16629  prmndvdsfaclt  16661  ncoprmlnprm  16663  fermltl  16716  pceu  16778  setsstruct2  17106  setsstruct  17108  mreexexd  17591  isglbd  18461  symgpssefmnd  19262  pmtrfrn  19325  psgnunilem4  19364  ablsimpgprmd  19984  mulgass2  20120  islss4  20572  lspsneu  20735  lspfixed  20740  lspexch  20741  lsmcv  20753  lspsolvlem  20754  xrsdsreclblem  20990  isphld  21206  mdetralt  22109  mdetunilem9  22121  fiinopn  22402  neips  22616  tpnei  22624  neindisj2  22626  opnneiid  22629  hausnei2  22856  cmpsublem  22902  cmpsub  22903  cmpcld  22905  comppfsc  23035  filufint  23423  cfinufil  23431  rnelfm  23456  alexsubALTlem1  23550  alexsubALTlem4  23553  alexsubALT  23554  tsmsxp  23658  neibl  24009  tngngp3  24172  tgqioo  24315  ovolunlem2  25014  iunmbl2  25073  itg1le  25230  vieta1  25824  aannenlem2  25841  aalioulem3  25846  aalioulem4  25847  aaliou2  25852  wilthlem3  26571  bcmono  26777  gausslemma2dlem1a  26865  sslttr  27305  ssltun1  27306  ssltun2  27307  sltlpss  27398  precsexlem8  27657  precsexlem9  27658  precsex  27661  iscgrglt  27762  axcontlem7  28225  elntg2  28240  edglnl  28400  numedglnl  28401  ausgrumgri  28424  ausgrusgri  28425  usgrausgrb  28426  usgredg2vtxeuALT  28476  ushgredgedg  28483  ushgredgedgloop  28485  nbuhgr2vtx1edgb  28606  cusgrsize2inds  28707  upgrewlkle2  28860  wlkl1loop  28892  redwlk  28926  pthdivtx  28983  pthdadjvtx  28984  upgr2pthnlp  28986  upgrspthswlk  28992  clwlkl1loop  29037  wwlksnred  29143  wwlksnextbi  29145  elwwlks2ons3im  29205  umgrwwlks2on  29208  clwwlknwwlksn  29288  clwwlkinwwlk  29290  wwlksext2clwwlk  29307  1pthon2v  29403  uhgr3cyclex  29432  n4cyclfrgr  29541  frgrwopreg  29573  numclwwlk1lem2f1  29607  clwwlknonclwlknonf1o  29612  wlkl0  29617  frgrreggt1  29643  frgrreg  29644  frgrregord013  29645  chintcli  30579  spansnss  30819  elspansn4  30821  chscllem4  30888  hoadddir  31052  adjmul  31340  kbass6  31369  spansncv2  31541  sumdmdii  31663  nexple  33002  bnj1417  34047  lfuhgr2  34104  cusgredgex  34107  sat1el2xp  34365  fmlasuc  34372  satffunlem1lem1  34388  satffunlem2lem1  34390  mclsind  34556  iprodefisumlem  34705  btwndiff  34994  elicc3  35197  finminlem  35198  sdclem2  36605  clmgmOLD  36714  grpomndo  36738  zerdivemp1x  36810  lsmsat  37873  lsmcv2  37894  lcvat  37895  lsatcveq0  37897  lcvexchlem4  37902  lcvexchlem5  37903  islshpcv  37918  l1cvpat  37919  lshpkrlem6  37980  omlfh3N  38124  cvlsupr4  38210  cvlsupr5  38211  cvlsupr6  38212  2llnneN  38275  hlrelat3  38278  cvrval3  38279  cvrval4N  38280  cvrexchlem  38285  2atlt  38305  cvrat4  38309  atbtwnexOLDN  38313  atbtwnex  38314  athgt  38322  3dim1  38333  3dim2  38334  3dim3  38335  1cvratex  38339  llnle  38384  atcvrlln2  38385  atcvrlln  38386  2llnmat  38390  lplnle  38406  lplnnle2at  38407  lplnnlelln  38409  llncvrlpln2  38423  2llnjN  38433  lvoli2  38447  lvolnlelln  38450  lvolnlelpln  38451  4atlem10  38472  4atlem11  38475  4atlem12  38478  lplncvrlvol2  38481  2lplnj  38486  lneq2at  38644  lnatexN  38645  lnjatN  38646  lncvrat  38648  2lnat  38650  cdlemb  38660  paddasslem14  38699  llnexchb2  38735  dalawlem10  38746  dalawlem13  38749  dalawlem14  38750  dalaw  38752  pclclN  38757  pclfinN  38766  osumcllem11N  38832  lhp2lt  38867  lhpexle3lem  38877  4atexlem7  38941  ldilcnv  38981  ldilco  38982  ltrncnv  39012  trlval2  39029  cdleme24  39218  cdleme26ee  39226  cdleme28  39239  cdleme32le  39313  cdleme50trn2  39417  cdleme50ltrn  39423  cdleme  39426  cdlemf1  39427  cdlemf  39429  cdlemg1cex  39454  cdlemg2ce  39458  cdlemg18b  39545  ltrnco  39585  tendocan  39690  cdlemk28-3  39774  cdlemk11t  39812  dia2dimlem6  39935  dia2dimlem12  39941  dihlsscpre  40100  dihord4  40124  dihord5b  40125  dihmeetlem3N  40171  dihmeetlem20N  40192  dvh4dimlem  40309  lclkrlem2y  40397  mapdpglem24  40570  mapdpglem32  40571  mapdpg  40572  baerlem3lem2  40576  baerlem5alem2  40577  baerlem5blem2  40578  mapdh9a  40655  mapdh9aOLDN  40656  hdmap14lem6  40739  hdmapglem7  40795  nnadddir  41186  nnmulcom  41188  nn0rppwr  41224  sn-addlid  41278  remulcand  41312  mzpexpmpt  41473  pellexlem5  41561  pellex  41563  pell14qrexpclnn0  41594  pellfundex  41614  monotuz  41670  monotoddzzfi  41671  rmxypos  41676  jm2.17a  41689  jm2.17b  41690  rmygeid  41693  jm2.19lem3  41720  jm2.15nn0  41732  jm2.16nn0  41733  aomclem2  41787  aomclem6  41791  dfac11  41794  hbtlem5  41860  cnsrexpcl  41897  cantnf2  42065  dflim5  42069  relexpxpnnidm  42444  relexpiidm  42445  relexpss1d  42446  iunrelexpmin1  42449  relexpmulnn  42450  iunrelexpmin2  42453  relexp01min  42454  relexp0a  42457  relexpxpmin  42458  relexpaddss  42459  trclimalb2  42467  tfindsd  42954  3impexpbicomi  43231  ee333  43258  eel12131  43464  eel2122old  43469  e333  43484  ordelordALTVD  43618  refsumcn  43704  uzwo4  43730  ssinc  43766  ssdec  43767  iunincfi  43773  restuni3  43797  eliuniin2  43799  rabssd  43821  reximdd  43831  suprnmpt  43860  disjf1o  43879  fompt  43880  disjinfi  43881  ssnnf1octb  43883  choicefi  43889  mapssbi  43902  unirnmapsn  43903  ssmapsn  43905  iunmapsn  43906  rnmptlb  43937  rnmptbddlem  43938  infnsuprnmpt  43944  fperiodmullem  44003  upbdrech  44005  ssfiunibd  44009  supxrgere  44033  iuneqfzuzlem  44034  supxrgelem  44037  supxrge  44038  suplesup  44039  infrpge  44051  infleinf  44072  suplesup2  44076  supxrunb3  44099  infleinf2  44114  rexabslelem  44118  infrnmptle  44123  infxrunb3rnmpt  44128  iccshift  44221  iooshift  44225  fmul01  44286  fmuldfeq  44289  fmul01lt1  44292  mullimc  44322  islptre  44325  mullimcf  44329  limcperiod  44334  islpcn  44345  limsupre  44347  limcleqr  44350  neglimc  44353  addlimc  44354  0ellimcdiv  44355  limclner  44357  fnlimfvre  44380  limsuppnflem  44416  limsupmnfuzlem  44432  limsupre3lem  44438  limsupre3uzlem  44441  climuzlem  44449  limsupgtlem  44483  coskpi2  44572  cosknegpi  44575  cncfshift  44580  cncfperiod  44585  icccncfext  44593  dvnmptdivc  44644  dvnmptconst  44647  dvnmul  44649  dvmptfprodlem  44650  dvmptfprod  44651  dvnprodlem1  44652  dvnprodlem2  44653  iblspltprt  44679  itgspltprt  44685  itgperiod  44687  ismbl3  44692  stoweidlem3  44709  stoweidlem31  44737  stoweidlem59  44765  stirlinglem13  44792  fourierdlem41  44854  fourierdlem42  44855  fourierdlem48  44860  fourierdlem51  44863  fourierdlem70  44882  fourierdlem71  44883  fourierdlem73  44885  fourierdlem80  44892  fourierdlem81  44893  fourierdlem89  44901  fourierdlem91  44903  fourierdlem93  44905  fourierdlem97  44909  elaa2  44940  qndenserrnopnlem  45003  salexct  45040  subsaliuncl  45064  subsalsal  45065  sge0tsms  45086  sge0f1o  45088  sge0fsum  45093  sge0supre  45095  sge0sup  45097  sge0rnbnd  45099  sge0gerp  45101  sge0pnffigt  45102  sge0lefi  45104  sge0ltfirp  45106  sge0resrn  45110  sge0resplit  45112  sge0split  45115  sge0iunmptlemfi  45119  sge0iunmptlemre  45121  sge0iunmpt  45124  sge0rpcpnf  45127  sge0isum  45133  sge0xp  45135  sge0xaddlem2  45140  sge0uzfsumgt  45150  sge0seq  45152  sge0reuz  45153  nnfoctbdjlem  45161  nnfoctbdj  45162  iundjiun  45166  meadjiunlem  45171  voliunsge0lem  45178  meaiuninclem  45186  meaiininc2  45194  carageniuncllem1  45227  carageniuncllem2  45228  caratheodorylem1  45232  caratheodorylem2  45233  isomenndlem  45236  ovnsupge0  45263  ovnlerp  45268  ovncvrrp  45270  ovnsubaddlem1  45276  hoidmvval0  45293  hoidmv1lelem3  45299  hoidmv1le  45300  hoidmvlelem1  45301  hoidmvlelem2  45302  hoidmvlelem3  45303  ovnhoilem2  45308  opnvonmbllem2  45339  ovnovollem3  45364  vonioo  45388  vonicc  45391  pimiooltgt  45416  sssmf  45444  smfaddlem1  45469  smflimlem6  45482  smfmullem4  45500  smfpimbor1lem1  45504  smfco  45508  smfpimcc  45514  smflimmpt  45516  smfinflem  45523  smflimsuplem7  45532  smflimsuplem8  45533  smflimsupmpt  45535  smfliminfmpt  45538  cfsetsnfsetf1  45759  elsetpreimafveqfv  46050  iccpartiltu  46080  sprsymrelfvlem  46148  reuopreuprim  46184  goldbachth  46205  fmtnofac1  46228  prmdvdsfmtnof1lem1  46242  lighneal  46269  isomgrsym  46494  isomgrtr  46497  uspgropssxp  46512  rnglidlmcl  46738  rngccatidALTV  46877  ringccatidALTV  46940  nzerooringczr  46960  lcosslsp  47109  fllog2  47244  dignn0flhalf  47294  fv1arycl  47313  1arymaptf1  47318  fv2arycl  47324  2arymaptf1  47329  itschlc0yqe  47436  itsclc0xyqsol  47444  seposep  47548  iscnrm3lem6  47561  iunord  47711  setrec2fun  47727