Theorem 3exp 1116

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3expb  1117  3expib  1119  3com12  1120  3com13  1121  pm3.2an3  1337  3exp1  1349  3expd  1350  exp5o  1352  3ecase  1471  rexlimdv3a  3245  rabssdv  4002  reupick2  4241  disjiund  5020  otiunsndisj  5375  wefrc  5513  predpo  6134  tz7.7  6185  unizlim  6275  fvelimad  6707  fveqdmss  6823  f1oiso2  7084  ssorduni  7480  suceloni  7508  tfisi  7553  funeldmdif  7729  poxp  7805  smo11  7984  tfrlem5  7999  odi  8188  omass  8189  nndi  8232  nnmass  8233  undifixp  8481  findcard  8741  ac6sfi  8746  domunfican  8775  mapfien2  8856  fisup2g  8916  fiinf2g  8948  indcardi  9452  acndom  9462  ackbij1lem16  9646  infpssrlem4  9717  fin23lem11  9728  isfin2-2  9730  fin23lem34  9757  fin1a2lem10  9820  hsmexlem2  9838  axcc3  9849  domtriomlem  9853  axdc3lem2  9862  axdc3lem4  9864  axcclem  9868  ttukeyg  9928  axdclem2  9931  axacndlem4  10021  axacndlem5  10022  axacnd  10023  tskr1om2  10179  tskwe2  10184  tskord  10191  tskcard  10192  tskuni  10194  tskwun  10195  gruiin  10221  grudomon  10228  gruina  10229  mulcanpi  10311  adderpq  10367  mulerpq  10368  dedekindle  10793  divgt0  11497  divge0  11498  nnne0  11659  uzind  12062  uzind2  12063  iccsplit  12863  ssnn0fi  13348  expmordi  13527  sqlecan  13567  modexp  13595  expnngt1  13598  facavg  13657  2cshwcshw  14178  relexpcnv  14386  relexpaddnn  14402  relexpaddg  14404  pwdif  15215  prodfn0  15242  prodfrec  15243  ntrivcvgfvn0  15247  fprodabs  15320  bpolycl  15398  bpolydif  15401  fprodefsum  15440  dvdsmodexp  15607  dvdsaddre2b  15649  dvdsnprmd  16024  2mulprm  16027  prmndvdsfaclt  16057  ncoprmlnprm  16058  fermltl  16111  pceu  16173  setsstruct2  16513  setsstruct  16515  mreexexd  16911  isglbd  17719  symgpssefmnd  18516  pmtrfrn  18578  psgnunilem4  18617  ablsimpgprmd  19230  mulgass2  19347  islss4  19727  lspsneu  19888  lspfixed  19893  lspexch  19894  lsmcv  19906  lspsolvlem  19907  xrsdsreclblem  20137  isphld  20343  mdetralt  21213  mdetunilem9  21225  fiinopn  21506  neips  21718  tpnei  21726  neindisj2  21728  opnneiid  21731  hausnei2  21958  cmpsublem  22004  cmpsub  22005  cmpcld  22007  comppfsc  22137  filufint  22525  cfinufil  22533  rnelfm  22558  alexsubALTlem1  22652  alexsubALTlem4  22655  alexsubALT  22656  tsmsxp  22760  neibl  23108  tngngp3  23262  tgqioo  23405  ovolunlem2  24102  iunmbl2  24161  itg1le  24317  vieta1  24908  aannenlem2  24925  aalioulem3  24930  aalioulem4  24931  aaliou2  24936  wilthlem3  25655  bcmono  25861  gausslemma2dlem1a  25949  iscgrglt  26308  axcontlem7  26764  elntg2  26779  edglnl  26936  numedglnl  26937  ausgrumgri  26960  ausgrusgri  26961  usgrausgrb  26962  usgredg2vtxeuALT  27012  ushgredgedg  27019  ushgredgedgloop  27021  nbuhgr2vtx1edgb  27142  cusgrsize2inds  27243  upgrewlkle2  27396  wlkl1loop  27427  redwlk  27462  pthdivtx  27518  pthdadjvtx  27519  upgr2pthnlp  27521  upgrspthswlk  27527  clwlkl1loop  27572  wwlksnred  27678  wwlksnextbi  27680  elwwlks2ons3im  27740  umgrwwlks2on  27743  clwwlknwwlksn  27823  clwwlkinwwlk  27825  wwlksext2clwwlk  27842  1pthon2v  27938  uhgr3cyclex  27967  n4cyclfrgr  28076  frgrwopreg  28108  numclwwlk1lem2f1  28142  clwwlknonclwlknonf1o  28147  wlkl0  28152  frgrreggt1  28178  frgrreg  28179  frgrregord013  28180  chintcli  29114  spansnss  29354  elspansn4  29356  chscllem4  29423  hoadddir  29587  adjmul  29875  kbass6  29904  spansncv2  30076  sumdmdii  30198  nexple  31378  bnj1417  32423  lfuhgr2  32478  cusgredgex  32481  sat1el2xp  32739  fmlasuc  32746  satffunlem1lem1  32762  satffunlem2lem1  32764  mclsind  32930  iprodefisumlem  33085  poseq  33208  fpr3g  33235  frrlem10  33245  btwndiff  33601  elicc3  33778  finminlem  33779  sdclem2  35180  clmgmOLD  35289  grpomndo  35313  zerdivemp1x  35385  lsmsat  36304  lsmcv2  36325  lcvat  36326  lsatcveq0  36328  lcvexchlem4  36333  lcvexchlem5  36334  islshpcv  36349  l1cvpat  36350  lshpkrlem6  36411  omlfh3N  36555  cvlsupr4  36641  cvlsupr5  36642  cvlsupr6  36643  2llnneN  36705  hlrelat3  36708  cvrval3  36709  cvrval4N  36710  cvrexchlem  36715  2atlt  36735  cvrat4  36739  atbtwnexOLDN  36743  atbtwnex  36744  athgt  36752  3dim1  36763  3dim2  36764  3dim3  36765  1cvratex  36769  llnle  36814  atcvrlln2  36815  atcvrlln  36816  2llnmat  36820  lplnle  36836  lplnnle2at  36837  lplnnlelln  36839  llncvrlpln2  36853  2llnjN  36863  lvoli2  36877  lvolnlelln  36880  lvolnlelpln  36881  4atlem10  36902  4atlem11  36905  4atlem12  36908  lplncvrlvol2  36911  2lplnj  36916  lneq2at  37074  lnatexN  37075  lnjatN  37076  lncvrat  37078  2lnat  37080  cdlemb  37090  paddasslem14  37129  llnexchb2  37165  dalawlem10  37176  dalawlem13  37179  dalawlem14  37180  dalaw  37182  pclclN  37187  pclfinN  37196  osumcllem11N  37262  lhp2lt  37297  lhpexle3lem  37307  4atexlem7  37371  ldilcnv  37411  ldilco  37412  ltrncnv  37442  trlval2  37459  cdleme24  37648  cdleme26ee  37656  cdleme28  37669  cdleme32le  37743  cdleme50trn2  37847  cdleme50ltrn  37853  cdleme  37856  cdlemf1  37857  cdlemf  37859  cdlemg1cex  37884  cdlemg2ce  37888  cdlemg18b  37975  ltrnco  38015  tendocan  38120  cdlemk28-3  38204  cdlemk11t  38242  dia2dimlem6  38365  dia2dimlem12  38371  dihlsscpre  38530  dihord4  38554  dihord5b  38555  dihmeetlem3N  38601  dihmeetlem20N  38622  dvh4dimlem  38739  lclkrlem2y  38827  mapdpglem24  39000  mapdpglem32  39001  mapdpg  39002  baerlem3lem2  39006  baerlem5alem2  39007  baerlem5blem2  39008  mapdh9a  39085  mapdh9aOLDN  39086  hdmap14lem6  39169  hdmapglem7  39225  nnadddir  39471  nnmulcom  39473  nn0rppwr  39490  sn-addid2  39542  remulcand  39575  mzpexpmpt  39686  pellexlem5  39774  pellex  39776  pell14qrexpclnn0  39807  pellfundex  39827  monotuz  39882  monotoddzzfi  39883  rmxypos  39888  jm2.17a  39901  jm2.17b  39902  rmygeid  39905  jm2.19lem3  39932  jm2.15nn0  39944  jm2.16nn0  39945  aomclem2  39999  aomclem6  40003  dfac11  40006  hbtlem5  40072  cnsrexpcl  40109  relexpxpnnidm  40404  relexpiidm  40405  relexpss1d  40406  iunrelexpmin1  40409  relexpmulnn  40410  iunrelexpmin2  40413  relexp01min  40414  relexp0a  40417  relexpxpmin  40418  relexpaddss  40419  trclimalb2  40427  tfindsd  40918  3impexpbicomi  41186  ee333  41213  eel12131  41419  eel2122old  41424  e333  41439  ordelordALTVD  41573  refsumcn  41659  uzwo4  41687  ssinc  41723  ssdec  41724  iunincfi  41730  restuni3  41753  eliuniin2  41755  rabssd  41779  reximdd  41789  suprnmpt  41798  disjf1o  41818  fompt  41819  disjinfi  41820  ssnnf1octb  41822  choicefi  41829  mapssbi  41842  unirnmapsn  41843  ssmapsn  41845  iunmapsn  41846  funimassd  41863  rnmptlb  41880  rnmptbddlem  41881  infnsuprnmpt  41888  fperiodmullem  41935  upbdrech  41937  ssfiunibd  41941  supxrgere  41965  iuneqfzuzlem  41966  supxrgelem  41969  supxrge  41970  suplesup  41971  infrpge  41983  infleinf  42004  suplesup2  42008  supxrunb3  42036  infleinf2  42051  rexabslelem  42055  infrnmptle  42060  infxrunb3rnmpt  42065  iccshift  42155  iooshift  42159  fmul01  42222  fmuldfeq  42225  fmul01lt1  42228  mullimc  42258  islptre  42261  mullimcf  42265  limcperiod  42270  islpcn  42281  limsupre  42283  limcleqr  42286  neglimc  42289  addlimc  42290  0ellimcdiv  42291  limclner  42293  fnlimfvre  42316  limsuppnflem  42352  limsupmnfuzlem  42368  limsupre3lem  42374  limsupre3uzlem  42377  climuzlem  42385  limsupgtlem  42419  coskpi2  42508  cosknegpi  42511  cncfshift  42516  cncfperiod  42521  icccncfext  42529  dvnmptdivc  42580  dvnmptconst  42583  dvnmul  42585  dvmptfprodlem  42586  dvmptfprod  42587  dvnprodlem1  42588  dvnprodlem2  42589  iblspltprt  42615  itgspltprt  42621  itgperiod  42623  ismbl3  42628  stoweidlem3  42645  stoweidlem31  42673  stoweidlem59  42701  stirlinglem13  42728  fourierdlem41  42790  fourierdlem42  42791  fourierdlem48  42796  fourierdlem51  42799  fourierdlem53  42801  fourierdlem70  42818  fourierdlem71  42819  fourierdlem73  42821  fourierdlem80  42828  fourierdlem81  42829  fourierdlem89  42837  fourierdlem91  42839  fourierdlem93  42841  fourierdlem97  42845  elaa2  42876  qndenserrnopnlem  42939  salexct  42974  subsaliuncl  42998  subsalsal  42999  sge0tsms  43019  sge0f1o  43021  sge0fsum  43026  sge0supre  43028  sge0sup  43030  sge0rnbnd  43032  sge0gerp  43034  sge0pnffigt  43035  sge0lefi  43037  sge0ltfirp  43039  sge0resrn  43043  sge0resplit  43045  sge0split  43048  sge0iunmptlemfi  43052  sge0iunmptlemre  43054  sge0iunmpt  43057  sge0rpcpnf  43060  sge0isum  43066  sge0xp  43068  sge0xaddlem2  43073  sge0uzfsumgt  43083  sge0seq  43085  sge0reuz  43086  nnfoctbdjlem  43094  nnfoctbdj  43095  iundjiun  43099  meadjiunlem  43104  voliunsge0lem  43111  meaiuninclem  43119  meaiininc2  43127  carageniuncllem1  43160  carageniuncllem2  43161  caratheodorylem1  43165  caratheodorylem2  43166  isomenndlem  43169  ovnsupge0  43196  ovnlerp  43201  ovncvrrp  43203  ovnsubaddlem1  43209  hoidmvval0  43226  hoidmv1lelem3  43232  hoidmv1le  43233  hoidmvlelem1  43234  hoidmvlelem2  43235  hoidmvlelem3  43236  ovnhoilem2  43241  opnvonmbllem2  43272  ovolval5lem3  43293  ovnovollem3  43297  vonioo  43321  vonicc  43324  pimiooltgt  43346  sssmf  43372  smfaddlem1  43396  smflimlem6  43409  smfmullem4  43426  smfpimbor1lem1  43430  smfco  43434  smfpimcc  43439  smflimmpt  43441  smfinflem  43448  smflimsuplem7  43457  smflimsuplem8  43458  smflimsupmpt  43460  smfliminfmpt  43463  elsetpreimafveqfv  43909  iccpartiltu  43939  sprsymrelfvlem  44007  reuopreuprim  44043  goldbachth  44064  fmtnofac1  44087  prmdvdsfmtnof1lem1  44101  lighneal  44129  isomgrsym  44354  isomgrtr  44357  uspgropssxp  44372  rngccatidALTV  44613  ringccatidALTV  44676  nzerooringczr  44696  lcosslsp  44847  fllog2  44982  dignn0flhalf  45032  fv1arycl  45051  1arymaptf1  45056  fv2arycl  45062  2arymaptf1  45067  itschlc0yqe  45174  itsclc0xyqsol  45182  iunord  45206  setrec2fun  45222