Theorem 3exp 1117

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 1116	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	exp31 419	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  3expb  1118  3expib  1120  3com12  1121  3com13  1122  pm3.2an3  1338  3exp1  1350  3expd  1351  exp5o  1353  3ecase  1472  rexlimdv3a  3214  rabssdv  4004  reupick2  4251  disjiund  5060  otiunsndisj  5428  wefrc  5574  tz7.7  6277  unizlim  6368  fvelimad  6818  fveqdmss  6938  f1oiso2  7203  ssorduni  7606  suceloni  7635  tfisi  7680  funeldmdif  7862  poxp  7940  fpr3g  8072  frrlem10  8082  smo11  8166  tfrlem5  8182  odi  8372  omass  8373  nndi  8416  nnmass  8417  undifixp  8680  findcard  8908  ac6sfi  8988  domunfican  9017  mapfien2  9098  fisup2g  9157  fiinf2g  9189  indcardi  9728  acndom  9738  ackbij1lem16  9922  infpssrlem4  9993  fin23lem11  10004  isfin2-2  10006  fin23lem34  10033  fin1a2lem10  10096  hsmexlem2  10114  axcc3  10125  domtriomlem  10129  axdc3lem2  10138  axdc3lem4  10140  axcclem  10144  ttukeyg  10204  axdclem2  10207  axacndlem4  10297  axacndlem5  10298  axacnd  10299  tskr1om2  10455  tskwe2  10460  tskord  10467  tskcard  10468  tskuni  10470  tskwun  10471  gruiin  10497  grudomon  10504  gruina  10505  mulcanpi  10587  adderpq  10643  mulerpq  10644  dedekindle  11069  divgt0  11773  divge0  11774  nnne0  11937  uzind  12342  uzind2  12343  iccsplit  13146  ssnn0fi  13633  expmordi  13813  sqlecan  13853  modexp  13881  expnngt1  13884  facavg  13943  2cshwcshw  14466  relexpcnv  14674  relexpaddnn  14690  relexpaddg  14692  pwdif  15508  prodfn0  15534  prodfrec  15535  ntrivcvgfvn0  15539  fprodabs  15612  bpolycl  15690  bpolydif  15693  fprodefsum  15732  dvdsmodexp  15899  dvdsaddre2b  15944  dvdsnprmd  16323  2mulprm  16326  prmndvdsfaclt  16358  ncoprmlnprm  16360  fermltl  16413  pceu  16475  setsstruct2  16803  setsstruct  16805  mreexexd  17274  isglbd  18142  symgpssefmnd  18918  pmtrfrn  18981  psgnunilem4  19020  ablsimpgprmd  19633  mulgass2  19755  islss4  20139  lspsneu  20300  lspfixed  20305  lspexch  20306  lsmcv  20318  lspsolvlem  20319  xrsdsreclblem  20556  isphld  20771  mdetralt  21665  mdetunilem9  21677  fiinopn  21958  neips  22172  tpnei  22180  neindisj2  22182  opnneiid  22185  hausnei2  22412  cmpsublem  22458  cmpsub  22459  cmpcld  22461  comppfsc  22591  filufint  22979  cfinufil  22987  rnelfm  23012  alexsubALTlem1  23106  alexsubALTlem4  23109  alexsubALT  23110  tsmsxp  23214  neibl  23563  tngngp3  23726  tgqioo  23869  ovolunlem2  24567  iunmbl2  24626  itg1le  24783  vieta1  25377  aannenlem2  25394  aalioulem3  25399  aalioulem4  25400  aaliou2  25405  wilthlem3  26124  bcmono  26330  gausslemma2dlem1a  26418  iscgrglt  26779  axcontlem7  27241  elntg2  27256  edglnl  27416  numedglnl  27417  ausgrumgri  27440  ausgrusgri  27441  usgrausgrb  27442  usgredg2vtxeuALT  27492  ushgredgedg  27499  ushgredgedgloop  27501  nbuhgr2vtx1edgb  27622  cusgrsize2inds  27723  upgrewlkle2  27876  wlkl1loop  27907  redwlk  27942  pthdivtx  27998  pthdadjvtx  27999  upgr2pthnlp  28001  upgrspthswlk  28007  clwlkl1loop  28052  wwlksnred  28158  wwlksnextbi  28160  elwwlks2ons3im  28220  umgrwwlks2on  28223  clwwlknwwlksn  28303  clwwlkinwwlk  28305  wwlksext2clwwlk  28322  1pthon2v  28418  uhgr3cyclex  28447  n4cyclfrgr  28556  frgrwopreg  28588  numclwwlk1lem2f1  28622  clwwlknonclwlknonf1o  28627  wlkl0  28632  frgrreggt1  28658  frgrreg  28659  frgrregord013  28660  chintcli  29594  spansnss  29834  elspansn4  29836  chscllem4  29903  hoadddir  30067  adjmul  30355  kbass6  30384  spansncv2  30556  sumdmdii  30678  nexple  31877  bnj1417  32921  lfuhgr2  32980  cusgredgex  32983  sat1el2xp  33241  fmlasuc  33248  satffunlem1lem1  33264  satffunlem2lem1  33266  mclsind  33432  iprodefisumlem  33612  ttrclss  33706  ttrclselem2  33712  poseq  33729  sslttr  33928  ssltun1  33929  ssltun2  33930  sltlpss  34014  btwndiff  34256  elicc3  34433  finminlem  34434  sdclem2  35827  clmgmOLD  35936  grpomndo  35960  zerdivemp1x  36032  lsmsat  36949  lsmcv2  36970  lcvat  36971  lsatcveq0  36973  lcvexchlem4  36978  lcvexchlem5  36979  islshpcv  36994  l1cvpat  36995  lshpkrlem6  37056  omlfh3N  37200  cvlsupr4  37286  cvlsupr5  37287  cvlsupr6  37288  2llnneN  37350  hlrelat3  37353  cvrval3  37354  cvrval4N  37355  cvrexchlem  37360  2atlt  37380  cvrat4  37384  atbtwnexOLDN  37388  atbtwnex  37389  athgt  37397  3dim1  37408  3dim2  37409  3dim3  37410  1cvratex  37414  llnle  37459  atcvrlln2  37460  atcvrlln  37461  2llnmat  37465  lplnle  37481  lplnnle2at  37482  lplnnlelln  37484  llncvrlpln2  37498  2llnjN  37508  lvoli2  37522  lvolnlelln  37525  lvolnlelpln  37526  4atlem10  37547  4atlem11  37550  4atlem12  37553  lplncvrlvol2  37556  2lplnj  37561  lneq2at  37719  lnatexN  37720  lnjatN  37721  lncvrat  37723  2lnat  37725  cdlemb  37735  paddasslem14  37774  llnexchb2  37810  dalawlem10  37821  dalawlem13  37824  dalawlem14  37825  dalaw  37827  pclclN  37832  pclfinN  37841  osumcllem11N  37907  lhp2lt  37942  lhpexle3lem  37952  4atexlem7  38016  ldilcnv  38056  ldilco  38057  ltrncnv  38087  trlval2  38104  cdleme24  38293  cdleme26ee  38301  cdleme28  38314  cdleme32le  38388  cdleme50trn2  38492  cdleme50ltrn  38498  cdleme  38501  cdlemf1  38502  cdlemf  38504  cdlemg1cex  38529  cdlemg2ce  38533  cdlemg18b  38620  ltrnco  38660  tendocan  38765  cdlemk28-3  38849  cdlemk11t  38887  dia2dimlem6  39010  dia2dimlem12  39016  dihlsscpre  39175  dihord4  39199  dihord5b  39200  dihmeetlem3N  39246  dihmeetlem20N  39267  dvh4dimlem  39384  lclkrlem2y  39472  mapdpglem24  39645  mapdpglem32  39646  mapdpg  39647  baerlem3lem2  39651  baerlem5alem2  39652  baerlem5blem2  39653  mapdh9a  39730  mapdh9aOLDN  39731  hdmap14lem6  39814  hdmapglem7  39870  nnadddir  40221  nnmulcom  40223  nn0rppwr  40254  sn-addid2  40308  remulcand  40341  mzpexpmpt  40483  pellexlem5  40571  pellex  40573  pell14qrexpclnn0  40604  pellfundex  40624  monotuz  40679  monotoddzzfi  40680  rmxypos  40685  jm2.17a  40698  jm2.17b  40699  rmygeid  40702  jm2.19lem3  40729  jm2.15nn0  40741  jm2.16nn0  40742  aomclem2  40796  aomclem6  40800  dfac11  40803  hbtlem5  40869  cnsrexpcl  40906  relexpxpnnidm  41200  relexpiidm  41201  relexpss1d  41202  iunrelexpmin1  41205  relexpmulnn  41206  iunrelexpmin2  41209  relexp01min  41210  relexp0a  41213  relexpxpmin  41214  relexpaddss  41215  trclimalb2  41223  tfindsd  41712  3impexpbicomi  41989  ee333  42016  eel12131  42222  eel2122old  42227  e333  42242  ordelordALTVD  42376  refsumcn  42462  uzwo4  42490  ssinc  42526  ssdec  42527  iunincfi  42533  restuni3  42556  eliuniin2  42558  rabssd  42580  reximdd  42590  suprnmpt  42599  disjf1o  42618  fompt  42619  disjinfi  42620  ssnnf1octb  42622  choicefi  42629  mapssbi  42642  unirnmapsn  42643  ssmapsn  42645  iunmapsn  42646  funimassd  42659  rnmptlb  42677  rnmptbddlem  42678  infnsuprnmpt  42685  fperiodmullem  42732  upbdrech  42734  ssfiunibd  42738  supxrgere  42762  iuneqfzuzlem  42763  supxrgelem  42766  supxrge  42767  suplesup  42768  infrpge  42780  infleinf  42801  suplesup2  42805  supxrunb3  42829  infleinf2  42844  rexabslelem  42848  infrnmptle  42853  infxrunb3rnmpt  42858  iccshift  42946  iooshift  42950  fmul01  43011  fmuldfeq  43014  fmul01lt1  43017  mullimc  43047  islptre  43050  mullimcf  43054  limcperiod  43059  islpcn  43070  limsupre  43072  limcleqr  43075  neglimc  43078  addlimc  43079  0ellimcdiv  43080  limclner  43082  fnlimfvre  43105  limsuppnflem  43141  limsupmnfuzlem  43157  limsupre3lem  43163  limsupre3uzlem  43166  climuzlem  43174  limsupgtlem  43208  coskpi2  43297  cosknegpi  43300  cncfshift  43305  cncfperiod  43310  icccncfext  43318  dvnmptdivc  43369  dvnmptconst  43372  dvnmul  43374  dvmptfprodlem  43375  dvmptfprod  43376  dvnprodlem1  43377  dvnprodlem2  43378  iblspltprt  43404  itgspltprt  43410  itgperiod  43412  ismbl3  43417  stoweidlem3  43434  stoweidlem31  43462  stoweidlem59  43490  stirlinglem13  43517  fourierdlem41  43579  fourierdlem42  43580  fourierdlem48  43585  fourierdlem51  43588  fourierdlem70  43607  fourierdlem71  43608  fourierdlem73  43610  fourierdlem80  43617  fourierdlem81  43618  fourierdlem89  43626  fourierdlem91  43628  fourierdlem93  43630  fourierdlem97  43634  elaa2  43665  qndenserrnopnlem  43728  salexct  43763  subsaliuncl  43787  subsalsal  43788  sge0tsms  43808  sge0f1o  43810  sge0fsum  43815  sge0supre  43817  sge0sup  43819  sge0rnbnd  43821  sge0gerp  43823  sge0pnffigt  43824  sge0lefi  43826  sge0ltfirp  43828  sge0resrn  43832  sge0resplit  43834  sge0split  43837  sge0iunmptlemfi  43841  sge0iunmptlemre  43843  sge0iunmpt  43846  sge0rpcpnf  43849  sge0isum  43855  sge0xp  43857  sge0xaddlem2  43862  sge0uzfsumgt  43872  sge0seq  43874  sge0reuz  43875  nnfoctbdjlem  43883  nnfoctbdj  43884  iundjiun  43888  meadjiunlem  43893  voliunsge0lem  43900  meaiuninclem  43908  meaiininc2  43916  carageniuncllem1  43949  carageniuncllem2  43950  caratheodorylem1  43954  caratheodorylem2  43955  isomenndlem  43958  ovnsupge0  43985  ovnlerp  43990  ovncvrrp  43992  ovnsubaddlem1  43998  hoidmvval0  44015  hoidmv1lelem3  44021  hoidmv1le  44022  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  ovnhoilem2  44030  opnvonmbllem2  44061  ovolval5lem3  44082  ovnovollem3  44086  vonioo  44110  vonicc  44113  pimiooltgt  44135  sssmf  44161  smfaddlem1  44185  smflimlem6  44198  smfmullem4  44215  smfpimbor1lem1  44219  smfco  44223  smfpimcc  44228  smflimmpt  44230  smfinflem  44237  smflimsuplem7  44246  smflimsuplem8  44247  smflimsupmpt  44249  smfliminfmpt  44252  cfsetsnfsetf1  44440  elsetpreimafveqfv  44732  iccpartiltu  44762  sprsymrelfvlem  44830  reuopreuprim  44866  goldbachth  44887  fmtnofac1  44910  prmdvdsfmtnof1lem1  44924  lighneal  44951  isomgrsym  45176  isomgrtr  45179  uspgropssxp  45194  rngccatidALTV  45435  ringccatidALTV  45498  nzerooringczr  45518  lcosslsp  45667  fllog2  45802  dignn0flhalf  45852  fv1arycl  45871  1arymaptf1  45876  fv2arycl  45882  2arymaptf1  45887  itschlc0yqe  45994  itsclc0xyqsol  46002  seposep  46107  iscnrm3lem6  46120  iunord  46268  setrec2fun  46284