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 418	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 395  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  3157  rabssdv  4073  reupick2  4321  disjiund  5139  otiunsndisj  5521  wefrc  5671  tz7.7  6391  unizlim  6488  funimassd  6959  fvelimad  6960  fveqdmss  7081  fompt  7120  f1oiso2  7353  ssorduni  7770  sucexeloniOLD  7802  suceloniOLD  7804  tfisi  7852  funeldmdif  8038  poxp  8118  poseq  8148  fpr3g  8274  frrlem10  8284  smo11  8368  tfrlem5  8384  odi  8583  omass  8584  nndi  8627  nnmass  8628  undifixp  8932  findcard  9167  php3  9216  ac6sfi  9291  domunfican  9324  mapfien2  9408  fisup2g  9467  fiinf2g  9499  ttrclss  9719  ttrclselem2  9725  indcardi  10040  acndom  10050  ackbij1lem16  10234  infpssrlem4  10305  fin23lem11  10316  isfin2-2  10318  fin23lem34  10345  fin1a2lem10  10408  hsmexlem2  10426  axcc3  10437  domtriomlem  10441  axdc3lem2  10450  axdc3lem4  10452  axcclem  10456  ttukeyg  10516  axdclem2  10519  axacndlem4  10609  axacndlem5  10610  axacnd  10611  tskr1om2  10767  tskwe2  10772  tskord  10779  tskcard  10780  tskuni  10782  tskwun  10783  gruiin  10809  grudomon  10816  gruina  10817  mulcanpi  10899  adderpq  10955  mulerpq  10956  dedekindle  11384  divgt0  12088  divge0  12089  nnne0  12252  uzind  12660  uzind2  12661  iccsplit  13468  ssnn0fi  13956  expmordi  14138  sqlecan  14179  modexp  14207  expnngt1  14210  facavg  14267  2cshwcshw  14782  relexpcnv  14988  relexpaddnn  15004  relexpaddg  15006  pwdif  15820  prodfn0  15846  prodfrec  15847  ntrivcvgfvn0  15851  fprodabs  15924  bpolycl  16002  bpolydif  16005  fprodefsum  16044  dvdsmodexp  16211  dvdsaddre2b  16256  dvdsnprmd  16633  2mulprm  16636  prmndvdsfaclt  16668  ncoprmlnprm  16670  fermltl  16723  pceu  16785  setsstruct2  17113  setsstruct  17115  mreexexd  17598  isglbd  18468  symgpssefmnd  19306  pmtrfrn  19369  psgnunilem4  19408  ablsimpgprmd  20028  mulgass2  20199  islss4  20719  lspsneu  20883  lspfixed  20888  lspexch  20889  lsmcv  20901  lspsolvlem  20902  rnglidlmcl  20984  xrsdsreclblem  21193  isphld  21428  mdetralt  22332  mdetunilem9  22344  fiinopn  22625  neips  22839  tpnei  22847  neindisj2  22849  opnneiid  22852  hausnei2  23079  cmpsublem  23125  cmpsub  23126  cmpcld  23128  comppfsc  23258  filufint  23646  cfinufil  23654  rnelfm  23679  alexsubALTlem1  23773  alexsubALTlem4  23776  alexsubALT  23777  tsmsxp  23881  neibl  24232  tngngp3  24395  tgqioo  24538  ovolunlem2  25249  iunmbl2  25308  itg1le  25465  vieta1  26059  aannenlem2  26076  aalioulem3  26081  aalioulem4  26082  aaliou2  26087  wilthlem3  26808  bcmono  27014  gausslemma2dlem1a  27102  sslttr  27543  ssltun1  27544  ssltun2  27545  sltlpss  27636  precsexlem8  27897  precsexlem9  27898  precsex  27901  iscgrglt  28030  axcontlem7  28493  elntg2  28508  edglnl  28668  numedglnl  28669  ausgrumgri  28692  ausgrusgri  28693  usgrausgrb  28694  usgredg2vtxeuALT  28744  ushgredgedg  28751  ushgredgedgloop  28753  nbuhgr2vtx1edgb  28874  cusgrsize2inds  28975  upgrewlkle2  29128  wlkl1loop  29160  redwlk  29194  pthdivtx  29251  pthdadjvtx  29252  upgr2pthnlp  29254  upgrspthswlk  29260  clwlkl1loop  29305  wwlksnred  29411  wwlksnextbi  29413  elwwlks2ons3im  29473  umgrwwlks2on  29476  clwwlknwwlksn  29556  clwwlkinwwlk  29558  wwlksext2clwwlk  29575  1pthon2v  29671  uhgr3cyclex  29700  n4cyclfrgr  29809  frgrwopreg  29841  numclwwlk1lem2f1  29875  clwwlknonclwlknonf1o  29880  wlkl0  29885  frgrreggt1  29911  frgrreg  29912  frgrregord013  29913  chintcli  30849  spansnss  31089  elspansn4  31091  chscllem4  31158  hoadddir  31322  adjmul  31610  kbass6  31639  spansncv2  31811  sumdmdii  31933  nexple  33303  bnj1417  34348  lfuhgr2  34405  cusgredgex  34408  sat1el2xp  34666  fmlasuc  34673  satffunlem1lem1  34689  satffunlem2lem1  34691  mclsind  34857  iprodefisumlem  35012  btwndiff  35301  elicc3  35507  finminlem  35508  sdclem2  36915  clmgmOLD  37024  grpomndo  37048  zerdivemp1x  37120  lsmsat  38183  lsmcv2  38204  lcvat  38205  lsatcveq0  38207  lcvexchlem4  38212  lcvexchlem5  38213  islshpcv  38228  l1cvpat  38229  lshpkrlem6  38290  omlfh3N  38434  cvlsupr4  38520  cvlsupr5  38521  cvlsupr6  38522  2llnneN  38585  hlrelat3  38588  cvrval3  38589  cvrval4N  38590  cvrexchlem  38595  2atlt  38615  cvrat4  38619  atbtwnexOLDN  38623  atbtwnex  38624  athgt  38632  3dim1  38643  3dim2  38644  3dim3  38645  1cvratex  38649  llnle  38694  atcvrlln2  38695  atcvrlln  38696  2llnmat  38700  lplnle  38716  lplnnle2at  38717  lplnnlelln  38719  llncvrlpln2  38733  2llnjN  38743  lvoli2  38757  lvolnlelln  38760  lvolnlelpln  38761  4atlem10  38782  4atlem11  38785  4atlem12  38788  lplncvrlvol2  38791  2lplnj  38796  lneq2at  38954  lnatexN  38955  lnjatN  38956  lncvrat  38958  2lnat  38960  cdlemb  38970  paddasslem14  39009  llnexchb2  39045  dalawlem10  39056  dalawlem13  39059  dalawlem14  39060  dalaw  39062  pclclN  39067  pclfinN  39076  osumcllem11N  39142  lhp2lt  39177  lhpexle3lem  39187  4atexlem7  39251  ldilcnv  39291  ldilco  39292  ltrncnv  39322  trlval2  39339  cdleme24  39528  cdleme26ee  39536  cdleme28  39549  cdleme32le  39623  cdleme50trn2  39727  cdleme50ltrn  39733  cdleme  39736  cdlemf1  39737  cdlemf  39739  cdlemg1cex  39764  cdlemg2ce  39768  cdlemg18b  39855  ltrnco  39895  tendocan  40000  cdlemk28-3  40084  cdlemk11t  40122  dia2dimlem6  40245  dia2dimlem12  40251  dihlsscpre  40410  dihord4  40434  dihord5b  40435  dihmeetlem3N  40481  dihmeetlem20N  40502  dvh4dimlem  40619  lclkrlem2y  40707  mapdpglem24  40880  mapdpglem32  40881  mapdpg  40882  baerlem3lem2  40886  baerlem5alem2  40887  baerlem5blem2  40888  mapdh9a  40965  mapdh9aOLDN  40966  hdmap14lem6  41049  hdmapglem7  41105  nnadddir  41488  nnmulcom  41490  nn0rppwr  41528  sn-addlid  41581  remulcand  41615  mzpexpmpt  41787  pellexlem5  41875  pellex  41877  pell14qrexpclnn0  41908  pellfundex  41928  monotuz  41984  monotoddzzfi  41985  rmxypos  41990  jm2.17a  42003  jm2.17b  42004  rmygeid  42007  jm2.19lem3  42034  jm2.15nn0  42046  jm2.16nn0  42047  aomclem2  42101  aomclem6  42105  dfac11  42108  hbtlem5  42174  cnsrexpcl  42211  cantnf2  42379  dflim5  42383  relexpxpnnidm  42758  relexpiidm  42759  relexpss1d  42760  iunrelexpmin1  42763  relexpmulnn  42764  iunrelexpmin2  42767  relexp01min  42768  relexp0a  42771  relexpxpmin  42772  relexpaddss  42773  trclimalb2  42781  tfindsd  43268  3impexpbicomi  43545  ee333  43572  eel12131  43778  eel2122old  43783  e333  43798  ordelordALTVD  43932  refsumcn  44018  uzwo4  44043  ssinc  44079  ssdec  44080  iunincfi  44086  restuni3  44110  eliuniin2  44112  rabssd  44134  reximdd  44144  suprnmpt  44173  disjf1o  44190  disjinfi  44191  ssnnf1octb  44193  choicefi  44199  mapssbi  44212  unirnmapsn  44213  ssmapsn  44215  iunmapsn  44216  rnmptlb  44247  rnmptbddlem  44248  infnsuprnmpt  44254  fperiodmullem  44313  upbdrech  44315  ssfiunibd  44319  supxrgere  44343  iuneqfzuzlem  44344  supxrgelem  44347  supxrge  44348  suplesup  44349  infrpge  44361  infleinf  44382  suplesup2  44386  supxrunb3  44409  infleinf2  44424  rexabslelem  44428  infrnmptle  44433  infxrunb3rnmpt  44438  iccshift  44531  iooshift  44535  fmul01  44596  fmuldfeq  44599  fmul01lt1  44602  mullimc  44632  islptre  44635  mullimcf  44639  limcperiod  44644  islpcn  44655  limsupre  44657  limcleqr  44660  neglimc  44663  addlimc  44664  0ellimcdiv  44665  limclner  44667  fnlimfvre  44690  limsuppnflem  44726  limsupmnfuzlem  44742  limsupre3lem  44748  limsupre3uzlem  44751  climuzlem  44759  limsupgtlem  44793  coskpi2  44882  cosknegpi  44885  cncfshift  44890  cncfperiod  44895  icccncfext  44903  dvnmptdivc  44954  dvnmptconst  44957  dvnmul  44959  dvmptfprodlem  44960  dvmptfprod  44961  dvnprodlem1  44962  dvnprodlem2  44963  iblspltprt  44989  itgspltprt  44995  itgperiod  44997  ismbl3  45002  stoweidlem3  45019  stoweidlem31  45047  stoweidlem59  45075  stirlinglem13  45102  fourierdlem41  45164  fourierdlem42  45165  fourierdlem48  45170  fourierdlem51  45173  fourierdlem70  45192  fourierdlem71  45193  fourierdlem73  45195  fourierdlem80  45202  fourierdlem81  45203  fourierdlem89  45211  fourierdlem91  45213  fourierdlem93  45215  fourierdlem97  45219  elaa2  45250  qndenserrnopnlem  45313  salexct  45350  subsaliuncl  45374  subsalsal  45375  sge0tsms  45396  sge0f1o  45398  sge0fsum  45403  sge0supre  45405  sge0sup  45407  sge0rnbnd  45409  sge0gerp  45411  sge0pnffigt  45412  sge0lefi  45414  sge0ltfirp  45416  sge0resrn  45420  sge0resplit  45422  sge0split  45425  sge0iunmptlemfi  45429  sge0iunmptlemre  45431  sge0iunmpt  45434  sge0rpcpnf  45437  sge0isum  45443  sge0xp  45445  sge0xaddlem2  45450  sge0uzfsumgt  45460  sge0seq  45462  sge0reuz  45463  nnfoctbdjlem  45471  nnfoctbdj  45472  iundjiun  45476  meadjiunlem  45481  voliunsge0lem  45488  meaiuninclem  45496  meaiininc2  45504  carageniuncllem1  45537  carageniuncllem2  45538  caratheodorylem1  45542  caratheodorylem2  45543  isomenndlem  45546  ovnsupge0  45573  ovnlerp  45578  ovncvrrp  45580  ovnsubaddlem1  45586  hoidmvval0  45603  hoidmv1lelem3  45609  hoidmv1le  45610  hoidmvlelem1  45611  hoidmvlelem2  45612  hoidmvlelem3  45613  ovnhoilem2  45618  opnvonmbllem2  45649  ovnovollem3  45674  vonioo  45698  vonicc  45701  pimiooltgt  45726  sssmf  45754  smfaddlem1  45779  smflimlem6  45792  smfmullem4  45810  smfpimbor1lem1  45814  smfco  45818  smfpimcc  45824  smflimmpt  45826  smfinflem  45833  smflimsuplem7  45842  smflimsuplem8  45843  smflimsupmpt  45845  smfliminfmpt  45848  cfsetsnfsetf1  46069  elsetpreimafveqfv  46360  iccpartiltu  46390  sprsymrelfvlem  46458  reuopreuprim  46494  goldbachth  46515  fmtnofac1  46538  prmdvdsfmtnof1lem1  46552  lighneal  46579  isomgrsym  46804  isomgrtr  46807  uspgropssxp  46822  rngccatidALTV  46977  ringccatidALTV  47040  nzerooringczr  47060  lcosslsp  47208  fllog2  47343  dignn0flhalf  47393  fv1arycl  47412  1arymaptf1  47417  fv2arycl  47423  2arymaptf1  47428  itschlc0yqe  47535  itsclc0xyqsol  47543  seposep  47647  iscnrm3lem6  47660  iunord  47810  setrec2fun  47826