Theorem 3exp 1118

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 1117	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	exp31 420	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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3expb  1119  3expib  1121  3com12  1122  3com13  1123  pm3.2an3  1339  3exp1  1351  3expd  1352  exp5o  1354  3ecase  1473  rexlimdv3a  3216  rabssdv  4009  reupick2  4255  disjiund  5065  otiunsndisj  5435  wefrc  5584  tz7.7  6296  unizlim  6387  fvelimad  6845  fveqdmss  6965  f1oiso2  7232  ssorduni  7638  sucexeloni  7667  suceloniOLD  7669  tfisi  7714  funeldmdif  7898  poxp  7978  fpr3g  8110  frrlem10  8120  smo11  8204  tfrlem5  8220  odi  8419  omass  8420  nndi  8463  nnmass  8464  undifixp  8731  findcard  8955  php3  9004  ac6sfi  9067  domunfican  9096  mapfien2  9177  fisup2g  9236  fiinf2g  9268  ttrclss  9487  ttrclselem2  9493  indcardi  9806  acndom  9816  ackbij1lem16  10000  infpssrlem4  10071  fin23lem11  10082  isfin2-2  10084  fin23lem34  10111  fin1a2lem10  10174  hsmexlem2  10192  axcc3  10203  domtriomlem  10207  axdc3lem2  10216  axdc3lem4  10218  axcclem  10222  ttukeyg  10282  axdclem2  10285  axacndlem4  10375  axacndlem5  10376  axacnd  10377  tskr1om2  10533  tskwe2  10538  tskord  10545  tskcard  10546  tskuni  10548  tskwun  10549  gruiin  10575  grudomon  10582  gruina  10583  mulcanpi  10665  adderpq  10721  mulerpq  10722  dedekindle  11148  divgt0  11852  divge0  11853  nnne0  12016  uzind  12421  uzind2  12422  iccsplit  13226  ssnn0fi  13714  expmordi  13894  sqlecan  13934  modexp  13962  expnngt1  13965  facavg  14024  2cshwcshw  14547  relexpcnv  14755  relexpaddnn  14771  relexpaddg  14773  pwdif  15589  prodfn0  15615  prodfrec  15616  ntrivcvgfvn0  15620  fprodabs  15693  bpolycl  15771  bpolydif  15774  fprodefsum  15813  dvdsmodexp  15980  dvdsaddre2b  16025  dvdsnprmd  16404  2mulprm  16407  prmndvdsfaclt  16439  ncoprmlnprm  16441  fermltl  16494  pceu  16556  setsstruct2  16884  setsstruct  16886  mreexexd  17366  isglbd  18236  symgpssefmnd  19012  pmtrfrn  19075  psgnunilem4  19114  ablsimpgprmd  19727  mulgass2  19849  islss4  20233  lspsneu  20394  lspfixed  20399  lspexch  20400  lsmcv  20412  lspsolvlem  20413  xrsdsreclblem  20653  isphld  20868  mdetralt  21766  mdetunilem9  21778  fiinopn  22059  neips  22273  tpnei  22281  neindisj2  22283  opnneiid  22286  hausnei2  22513  cmpsublem  22559  cmpsub  22560  cmpcld  22562  comppfsc  22692  filufint  23080  cfinufil  23088  rnelfm  23113  alexsubALTlem1  23207  alexsubALTlem4  23210  alexsubALT  23211  tsmsxp  23315  neibl  23666  tngngp3  23829  tgqioo  23972  ovolunlem2  24671  iunmbl2  24730  itg1le  24887  vieta1  25481  aannenlem2  25498  aalioulem3  25503  aalioulem4  25504  aaliou2  25509  wilthlem3  26228  bcmono  26434  gausslemma2dlem1a  26522  iscgrglt  26884  axcontlem7  27347  elntg2  27362  edglnl  27522  numedglnl  27523  ausgrumgri  27546  ausgrusgri  27547  usgrausgrb  27548  usgredg2vtxeuALT  27598  ushgredgedg  27605  ushgredgedgloop  27607  nbuhgr2vtx1edgb  27728  cusgrsize2inds  27829  upgrewlkle2  27982  wlkl1loop  28014  redwlk  28049  pthdivtx  28106  pthdadjvtx  28107  upgr2pthnlp  28109  upgrspthswlk  28115  clwlkl1loop  28160  wwlksnred  28266  wwlksnextbi  28268  elwwlks2ons3im  28328  umgrwwlks2on  28331  clwwlknwwlksn  28411  clwwlkinwwlk  28413  wwlksext2clwwlk  28430  1pthon2v  28526  uhgr3cyclex  28555  n4cyclfrgr  28664  frgrwopreg  28696  numclwwlk1lem2f1  28730  clwwlknonclwlknonf1o  28735  wlkl0  28740  frgrreggt1  28766  frgrreg  28767  frgrregord013  28768  chintcli  29702  spansnss  29942  elspansn4  29944  chscllem4  30011  hoadddir  30175  adjmul  30463  kbass6  30492  spansncv2  30664  sumdmdii  30786  nexple  31986  bnj1417  33030  lfuhgr2  33089  cusgredgex  33092  sat1el2xp  33350  fmlasuc  33357  satffunlem1lem1  33373  satffunlem2lem1  33375  mclsind  33541  iprodefisumlem  33715  poseq  33811  sslttr  34010  ssltun1  34011  ssltun2  34012  sltlpss  34096  btwndiff  34338  elicc3  34515  finminlem  34516  sdclem2  35909  clmgmOLD  36018  grpomndo  36042  zerdivemp1x  36114  lsmsat  37029  lsmcv2  37050  lcvat  37051  lsatcveq0  37053  lcvexchlem4  37058  lcvexchlem5  37059  islshpcv  37074  l1cvpat  37075  lshpkrlem6  37136  omlfh3N  37280  cvlsupr4  37366  cvlsupr5  37367  cvlsupr6  37368  2llnneN  37430  hlrelat3  37433  cvrval3  37434  cvrval4N  37435  cvrexchlem  37440  2atlt  37460  cvrat4  37464  atbtwnexOLDN  37468  atbtwnex  37469  athgt  37477  3dim1  37488  3dim2  37489  3dim3  37490  1cvratex  37494  llnle  37539  atcvrlln2  37540  atcvrlln  37541  2llnmat  37545  lplnle  37561  lplnnle2at  37562  lplnnlelln  37564  llncvrlpln2  37578  2llnjN  37588  lvoli2  37602  lvolnlelln  37605  lvolnlelpln  37606  4atlem10  37627  4atlem11  37630  4atlem12  37633  lplncvrlvol2  37636  2lplnj  37641  lneq2at  37799  lnatexN  37800  lnjatN  37801  lncvrat  37803  2lnat  37805  cdlemb  37815  paddasslem14  37854  llnexchb2  37890  dalawlem10  37901  dalawlem13  37904  dalawlem14  37905  dalaw  37907  pclclN  37912  pclfinN  37921  osumcllem11N  37987  lhp2lt  38022  lhpexle3lem  38032  4atexlem7  38096  ldilcnv  38136  ldilco  38137  ltrncnv  38167  trlval2  38184  cdleme24  38373  cdleme26ee  38381  cdleme28  38394  cdleme32le  38468  cdleme50trn2  38572  cdleme50ltrn  38578  cdleme  38581  cdlemf1  38582  cdlemf  38584  cdlemg1cex  38609  cdlemg2ce  38613  cdlemg18b  38700  ltrnco  38740  tendocan  38845  cdlemk28-3  38929  cdlemk11t  38967  dia2dimlem6  39090  dia2dimlem12  39096  dihlsscpre  39255  dihord4  39279  dihord5b  39280  dihmeetlem3N  39326  dihmeetlem20N  39347  dvh4dimlem  39464  lclkrlem2y  39552  mapdpglem24  39725  mapdpglem32  39726  mapdpg  39727  baerlem3lem2  39731  baerlem5alem2  39732  baerlem5blem2  39733  mapdh9a  39810  mapdh9aOLDN  39811  hdmap14lem6  39894  hdmapglem7  39950  nnadddir  40307  nnmulcom  40309  nn0rppwr  40340  sn-addid2  40394  remulcand  40427  mzpexpmpt  40574  pellexlem5  40662  pellex  40664  pell14qrexpclnn0  40695  pellfundex  40715  monotuz  40770  monotoddzzfi  40771  rmxypos  40776  jm2.17a  40789  jm2.17b  40790  rmygeid  40793  jm2.19lem3  40820  jm2.15nn0  40832  jm2.16nn0  40833  aomclem2  40887  aomclem6  40891  dfac11  40894  hbtlem5  40960  cnsrexpcl  40997  relexpxpnnidm  41318  relexpiidm  41319  relexpss1d  41320  iunrelexpmin1  41323  relexpmulnn  41324  iunrelexpmin2  41327  relexp01min  41328  relexp0a  41331  relexpxpmin  41332  relexpaddss  41333  trclimalb2  41341  tfindsd  41830  3impexpbicomi  42107  ee333  42134  eel12131  42340  eel2122old  42345  e333  42360  ordelordALTVD  42494  refsumcn  42580  uzwo4  42608  ssinc  42644  ssdec  42645  iunincfi  42651  restuni3  42674  eliuniin2  42676  rabssd  42698  reximdd  42708  suprnmpt  42717  disjf1o  42736  fompt  42737  disjinfi  42738  ssnnf1octb  42740  choicefi  42747  mapssbi  42760  unirnmapsn  42761  ssmapsn  42763  iunmapsn  42764  funimassd  42777  rnmptlb  42795  rnmptbddlem  42796  infnsuprnmpt  42803  fperiodmullem  42849  upbdrech  42851  ssfiunibd  42855  supxrgere  42879  iuneqfzuzlem  42880  supxrgelem  42883  supxrge  42884  suplesup  42885  infrpge  42897  infleinf  42918  suplesup2  42922  supxrunb3  42946  infleinf2  42961  rexabslelem  42965  infrnmptle  42970  infxrunb3rnmpt  42975  iccshift  43063  iooshift  43067  fmul01  43128  fmuldfeq  43131  fmul01lt1  43134  mullimc  43164  islptre  43167  mullimcf  43171  limcperiod  43176  islpcn  43187  limsupre  43189  limcleqr  43192  neglimc  43195  addlimc  43196  0ellimcdiv  43197  limclner  43199  fnlimfvre  43222  limsuppnflem  43258  limsupmnfuzlem  43274  limsupre3lem  43280  limsupre3uzlem  43283  climuzlem  43291  limsupgtlem  43325  coskpi2  43414  cosknegpi  43417  cncfshift  43422  cncfperiod  43427  icccncfext  43435  dvnmptdivc  43486  dvnmptconst  43489  dvnmul  43491  dvmptfprodlem  43492  dvmptfprod  43493  dvnprodlem1  43494  dvnprodlem2  43495  iblspltprt  43521  itgspltprt  43527  itgperiod  43529  ismbl3  43534  stoweidlem3  43551  stoweidlem31  43579  stoweidlem59  43607  stirlinglem13  43634  fourierdlem41  43696  fourierdlem42  43697  fourierdlem48  43702  fourierdlem51  43705  fourierdlem70  43724  fourierdlem71  43725  fourierdlem73  43727  fourierdlem80  43734  fourierdlem81  43735  fourierdlem89  43743  fourierdlem91  43745  fourierdlem93  43747  fourierdlem97  43751  elaa2  43782  qndenserrnopnlem  43845  salexct  43880  subsaliuncl  43904  subsalsal  43905  sge0tsms  43925  sge0f1o  43927  sge0fsum  43932  sge0supre  43934  sge0sup  43936  sge0rnbnd  43938  sge0gerp  43940  sge0pnffigt  43941  sge0lefi  43943  sge0ltfirp  43945  sge0resrn  43949  sge0resplit  43951  sge0split  43954  sge0iunmptlemfi  43958  sge0iunmptlemre  43960  sge0iunmpt  43963  sge0rpcpnf  43966  sge0isum  43972  sge0xp  43974  sge0xaddlem2  43979  sge0uzfsumgt  43989  sge0seq  43991  sge0reuz  43992  nnfoctbdjlem  44000  nnfoctbdj  44001  iundjiun  44005  meadjiunlem  44010  voliunsge0lem  44017  meaiuninclem  44025  meaiininc2  44033  carageniuncllem1  44066  carageniuncllem2  44067  caratheodorylem1  44071  caratheodorylem2  44072  isomenndlem  44075  ovnsupge0  44102  ovnlerp  44107  ovncvrrp  44109  ovnsubaddlem1  44115  hoidmvval0  44132  hoidmv1lelem3  44138  hoidmv1le  44139  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem3  44142  ovnhoilem2  44147  opnvonmbllem2  44178  ovolval5lem3  44199  ovnovollem3  44203  vonioo  44227  vonicc  44230  pimiooltgt  44255  sssmf  44283  smfaddlem1  44308  smflimlem6  44321  smfmullem4  44339  smfpimbor1lem1  44343  smfco  44347  smfpimcc  44352  smflimmpt  44354  smfinflem  44361  smflimsuplem7  44370  smflimsuplem8  44371  smflimsupmpt  44373  smfliminfmpt  44376  cfsetsnfsetf1  44564  elsetpreimafveqfv  44855  iccpartiltu  44885  sprsymrelfvlem  44953  reuopreuprim  44989  goldbachth  45010  fmtnofac1  45033  prmdvdsfmtnof1lem1  45047  lighneal  45074  isomgrsym  45299  isomgrtr  45302  uspgropssxp  45317  rngccatidALTV  45558  ringccatidALTV  45621  nzerooringczr  45641  lcosslsp  45790  fllog2  45925  dignn0flhalf  45975  fv1arycl  45994  1arymaptf1  45999  fv2arycl  46005  2arymaptf1  46010  itschlc0yqe  46117  itsclc0xyqsol  46125  seposep  46230  iscnrm3lem6  46243  iunord  46393  setrec2fun  46409