Theorem 3exp 1115

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3expb  1116  3expib  1118  3com12  1119  3com13  1120  pm3.2an3  1336  3exp1  1348  3expd  1349  exp5o  1351  3ecase  1470  rexlimdv3a  3286  rabssdv  4051  reupick2  4289  disjiund  5056  otiunsndisj  5410  wefrc  5549  predpo  6166  tz7.7  6217  unizlim  6307  fvelimad  6732  fveqdmss  6846  f1oiso2  7105  ssorduni  7500  suceloni  7528  tfisi  7573  funeldmdif  7747  poxp  7822  smo11  8001  tfrlem5  8016  odi  8205  omass  8206  nndi  8249  nnmass  8250  undifixp  8498  findcard  8757  ac6sfi  8762  domunfican  8791  mapfien2  8872  fisup2g  8932  fiinf2g  8964  indcardi  9467  acndom  9477  ackbij1lem16  9657  infpssrlem4  9728  fin23lem11  9739  isfin2-2  9741  fin23lem34  9768  fin1a2lem10  9831  hsmexlem2  9849  axcc3  9860  domtriomlem  9864  axdc3lem2  9873  axdc3lem4  9875  axcclem  9879  ttukeyg  9939  axdclem2  9942  axacndlem4  10032  axacndlem5  10033  axacnd  10034  tskr1om2  10190  tskwe2  10195  tskord  10202  tskcard  10203  tskuni  10205  tskwun  10206  gruiin  10232  grudomon  10239  gruina  10240  mulcanpi  10322  adderpq  10378  mulerpq  10379  dedekindle  10804  divgt0  11508  divge0  11509  nnne0  11672  uzind  12075  uzind2  12076  iccsplit  12872  ssnn0fi  13354  expmordi  13532  sqlecan  13572  modexp  13600  expnngt1  13603  facavg  13662  2cshwcshw  14187  relexpcnv  14394  relexpreld  14399  relexpaddnn  14410  relexpaddg  14412  pwdif  15223  prodfn0  15250  prodfrec  15251  ntrivcvgfvn0  15255  fprodabs  15328  bpolycl  15406  bpolydif  15409  fprodefsum  15448  dvdsmodexp  15615  dvdsaddre2b  15657  dvdsnprmd  16034  2mulprm  16037  prmndvdsfaclt  16067  ncoprmlnprm  16068  fermltl  16121  pceu  16183  setsstruct2  16521  setsstruct  16523  mreexexd  16919  isglbd  17727  symgpssefmnd  18524  pmtrfrn  18586  psgnunilem4  18625  ablsimpgprmd  19237  mulgass2  19351  islss4  19734  lspsneu  19895  lspfixed  19900  lspexch  19901  lsmcv  19913  lspsolvlem  19914  xrsdsreclblem  20591  isphld  20798  mdetralt  21217  mdetunilem9  21229  fiinopn  21509  neips  21721  tpnei  21729  neindisj2  21731  opnneiid  21734  hausnei2  21961  cmpsublem  22007  cmpsub  22008  cmpcld  22010  comppfsc  22140  filufint  22528  cfinufil  22536  rnelfm  22561  alexsubALTlem1  22655  alexsubALTlem4  22658  alexsubALT  22659  tsmsxp  22763  neibl  23111  tngngp3  23265  tgqioo  23408  ovolunlem2  24099  iunmbl2  24158  itg1le  24314  vieta1  24901  aannenlem2  24918  aalioulem3  24923  aalioulem4  24924  aaliou2  24929  wilthlem3  25647  bcmono  25853  gausslemma2dlem1a  25941  iscgrglt  26300  axcontlem7  26756  elntg2  26771  edglnl  26928  numedglnl  26929  ausgrumgri  26952  ausgrusgri  26953  usgrausgrb  26954  usgredg2vtxeuALT  27004  ushgredgedg  27011  ushgredgedgloop  27013  nbuhgr2vtx1edgb  27134  cusgrsize2inds  27235  upgrewlkle2  27388  wlkl1loop  27419  redwlk  27454  pthdivtx  27510  pthdadjvtx  27511  upgr2pthnlp  27513  upgrspthswlk  27519  clwlkl1loop  27564  wwlksnred  27670  wwlksnextbi  27672  elwwlks2ons3im  27733  umgrwwlks2on  27736  clwwlknwwlksn  27816  clwwlkinwwlk  27818  wwlksext2clwwlk  27836  1pthon2v  27932  uhgr3cyclex  27961  n4cyclfrgr  28070  frgrwopreg  28102  numclwwlk1lem2f1  28136  clwwlknonclwlknonf1o  28141  wlkl0  28146  frgrreggt1  28172  frgrreg  28173  frgrregord013  28174  chintcli  29108  spansnss  29348  elspansn4  29350  chscllem4  29417  hoadddir  29581  adjmul  29869  kbass6  29898  spansncv2  30070  sumdmdii  30192  nexple  31268  bnj1417  32313  lfuhgr2  32365  cusgredgex  32368  sat1el2xp  32626  fmlasuc  32633  satffunlem1lem1  32649  satffunlem2lem1  32651  mclsind  32817  iprodefisumlem  32972  poseq  33095  fpr3g  33122  frrlem10  33132  btwndiff  33488  elicc3  33665  finminlem  33666  sdclem2  35032  clmgmOLD  35144  grpomndo  35168  zerdivemp1x  35240  lsmsat  36159  lsmcv2  36180  lcvat  36181  lsatcveq0  36183  lcvexchlem4  36188  lcvexchlem5  36189  islshpcv  36204  l1cvpat  36205  lshpkrlem6  36266  omlfh3N  36410  cvlsupr4  36496  cvlsupr5  36497  cvlsupr6  36498  2llnneN  36560  hlrelat3  36563  cvrval3  36564  cvrval4N  36565  cvrexchlem  36570  2atlt  36590  cvrat4  36594  atbtwnexOLDN  36598  atbtwnex  36599  athgt  36607  3dim1  36618  3dim2  36619  3dim3  36620  1cvratex  36624  llnle  36669  atcvrlln2  36670  atcvrlln  36671  2llnmat  36675  lplnle  36691  lplnnle2at  36692  lplnnlelln  36694  llncvrlpln2  36708  2llnjN  36718  lvoli2  36732  lvolnlelln  36735  lvolnlelpln  36736  4atlem10  36757  4atlem11  36760  4atlem12  36763  lplncvrlvol2  36766  2lplnj  36771  lneq2at  36929  lnatexN  36930  lnjatN  36931  lncvrat  36933  2lnat  36935  cdlemb  36945  paddasslem14  36984  llnexchb2  37020  dalawlem10  37031  dalawlem13  37034  dalawlem14  37035  dalaw  37037  pclclN  37042  pclfinN  37051  osumcllem11N  37117  lhp2lt  37152  lhpexle3lem  37162  4atexlem7  37226  ldilcnv  37266  ldilco  37267  ltrncnv  37297  trlval2  37314  cdleme24  37503  cdleme26ee  37511  cdleme28  37524  cdleme32le  37598  cdleme50trn2  37702  cdleme50ltrn  37708  cdleme  37711  cdlemf1  37712  cdlemf  37714  cdlemg1cex  37739  cdlemg2ce  37743  cdlemg18b  37830  ltrnco  37870  tendocan  37975  cdlemk28-3  38059  cdlemk11t  38097  dia2dimlem6  38220  dia2dimlem12  38226  dihlsscpre  38385  dihord4  38409  dihord5b  38410  dihmeetlem3N  38456  dihmeetlem20N  38477  dvh4dimlem  38594  lclkrlem2y  38682  mapdpglem24  38855  mapdpglem32  38856  mapdpg  38857  baerlem3lem2  38861  baerlem5alem2  38862  baerlem5blem2  38863  mapdh9a  38940  mapdh9aOLDN  38941  hdmap14lem6  39024  hdmapglem7  39080  nnadddir  39212  nnmulcom  39214  nn0rppwr  39231  sn-addid2  39283  remulcand  39299  mzpexpmpt  39391  pellexlem5  39479  pellex  39481  pell14qrexpclnn0  39512  pellfundex  39532  monotuz  39587  monotoddzzfi  39588  rmxypos  39593  jm2.17a  39606  jm2.17b  39607  rmygeid  39610  jm2.19lem3  39637  jm2.15nn0  39649  jm2.16nn0  39650  aomclem2  39704  aomclem6  39708  dfac11  39711  hbtlem5  39777  cnsrexpcl  39814  relexpxpnnidm  40097  relexpiidm  40098  relexpss1d  40099  iunrelexpmin1  40102  relexpmulnn  40103  iunrelexpmin2  40106  relexp01min  40107  relexp0a  40110  relexpxpmin  40111  relexpaddss  40112  trclimalb2  40120  tfindsd  40613  3impexpbicomi  40863  ee333  40890  eel12131  41096  eel2122old  41101  e333  41116  ordelordALTVD  41250  refsumcn  41336  uzwo4  41364  ssinc  41402  ssdec  41403  iunincfi  41409  restuni3  41433  eliuniin2  41435  rabssd  41460  reximdd  41470  suprnmpt  41479  disjf1o  41501  fompt  41502  disjinfi  41503  ssnnf1octb  41505  choicefi  41512  mapssbi  41525  unirnmapsn  41526  ssmapsn  41528  iunmapsn  41529  funimassd  41546  rnmptlb  41563  rnmptbddlem  41564  infnsuprnmpt  41571  fperiodmullem  41619  upbdrech  41621  ssfiunibd  41625  supxrgere  41650  iuneqfzuzlem  41651  supxrgelem  41654  supxrge  41655  suplesup  41656  infrpge  41668  infleinf  41689  suplesup2  41693  supxrunb3  41721  infleinf2  41737  rexabslelem  41741  infrnmptle  41746  infxrunb3rnmpt  41751  iccshift  41843  iooshift  41847  fmul01  41910  fmuldfeq  41913  fmul01lt1  41916  mullimc  41946  islptre  41949  mullimcf  41953  limcperiod  41958  islpcn  41969  limsupre  41971  limcleqr  41974  neglimc  41977  addlimc  41978  0ellimcdiv  41979  limclner  41981  fnlimfvre  42004  limsuppnflem  42040  limsupmnfuzlem  42056  limsupre3lem  42062  limsupre3uzlem  42065  climuzlem  42073  limsupgtlem  42107  coskpi2  42196  cosknegpi  42199  cncfshift  42206  cncfperiod  42211  icccncfext  42219  dvnmptdivc  42272  dvnmptconst  42275  dvnmul  42277  dvmptfprodlem  42278  dvmptfprod  42279  dvnprodlem1  42280  dvnprodlem2  42281  iblspltprt  42307  itgspltprt  42313  itgperiod  42315  ismbl3  42320  stoweidlem3  42337  stoweidlem31  42365  stoweidlem59  42393  stirlinglem13  42420  fourierdlem41  42482  fourierdlem42  42483  fourierdlem48  42488  fourierdlem51  42491  fourierdlem53  42493  fourierdlem70  42510  fourierdlem71  42511  fourierdlem73  42513  fourierdlem80  42520  fourierdlem81  42521  fourierdlem89  42529  fourierdlem91  42531  fourierdlem93  42533  fourierdlem97  42537  elaa2  42568  qndenserrnopnlem  42631  salexct  42666  subsaliuncl  42690  subsalsal  42691  sge0tsms  42711  sge0f1o  42713  sge0fsum  42718  sge0supre  42720  sge0sup  42722  sge0rnbnd  42724  sge0gerp  42726  sge0pnffigt  42727  sge0lefi  42729  sge0ltfirp  42731  sge0resrn  42735  sge0resplit  42737  sge0split  42740  sge0iunmptlemfi  42744  sge0iunmptlemre  42746  sge0iunmpt  42749  sge0rpcpnf  42752  sge0isum  42758  sge0xp  42760  sge0xaddlem2  42765  sge0uzfsumgt  42775  sge0seq  42777  sge0reuz  42778  nnfoctbdjlem  42786  nnfoctbdj  42787  iundjiun  42791  meadjiunlem  42796  voliunsge0lem  42803  meaiuninclem  42811  meaiininc2  42819  carageniuncllem1  42852  carageniuncllem2  42853  caratheodorylem1  42857  caratheodorylem2  42858  isomenndlem  42861  ovnsupge0  42888  ovnlerp  42893  ovncvrrp  42895  ovnsubaddlem1  42901  hoidmvval0  42918  hoidmv1lelem3  42924  hoidmv1le  42925  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem3  42928  ovnhoilem2  42933  opnvonmbllem2  42964  ovolval5lem3  42985  ovnovollem3  42989  vonioo  43013  vonicc  43016  pimiooltgt  43038  sssmf  43064  smfaddlem1  43088  smflimlem6  43101  smfmullem4  43118  smfpimbor1lem1  43122  smfco  43126  smfpimcc  43131  smflimmpt  43133  smfinflem  43140  smflimsuplem7  43149  smflimsuplem8  43150  smflimsupmpt  43152  smfliminfmpt  43155  elsetpreimafveqfv  43601  iccpartiltu  43631  sprsymrelfvlem  43701  reuopreuprim  43737  goldbachth  43758  fmtnofac1  43781  prmdvdsfmtnof1lem1  43795  lighneal  43825  isomgrsym  44050  isomgrtr  44053  uspgropssxp  44068  rngccatidALTV  44309  ringccatidALTV  44372  nzerooringczr  44392  lcosslsp  44542  fllog2  44677  dignn0flhalf  44727  itschlc0yqe  44796  itsclc0xyqsol  44804  iunord  44828  setrec2fun  44844