Theorem 3exp 1119

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 1118	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	exp31 419	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3expb  1120  3expib  1122  3com12  1123  3com13  1124  pm3.2an3  1341  3exp1  1353  3expd  1354  exp5o  1356  3ecase  1476  rexlimdv3a  3134  rabssdv  4026  reupick2  4282  disjiund  5083  otiunsndisj  5463  wefrc  5613  tz7.7  6333  unizlim  6431  funimassd  6889  fvelimad  6890  fveqdmss  7012  fompt  7052  f1oiso2  7289  ssorduni  7715  tfisi  7792  resf1extb  7867  funeldmdif  7983  poxp  8061  poseq  8091  fpr3g  8218  frrlem10  8228  smo11  8287  tfrlem5  8302  odi  8497  omass  8498  nndi  8541  nnmass  8542  naddoa  8620  undifixp  8861  findcard  9077  php3  9123  ac6sfi  9173  domunfican  9211  mapfien2  9299  fisup2g  9359  fiinf2g  9392  ttrclss  9616  ttrclselem2  9622  indcardi  9935  acndom  9945  ackbij1lem16  10128  infpssrlem4  10200  fin23lem11  10211  isfin2-2  10213  fin23lem34  10240  fin1a2lem10  10303  hsmexlem2  10321  axcc3  10332  domtriomlem  10336  axdc3lem2  10345  axdc3lem4  10347  axcclem  10351  ttukeyg  10411  axdclem2  10414  axacndlem4  10504  axacndlem5  10505  axacnd  10506  tskr1om2  10662  tskwe2  10667  tskord  10674  tskcard  10675  tskuni  10677  tskwun  10678  gruiin  10704  grudomon  10711  gruina  10712  mulcanpi  10794  adderpq  10850  mulerpq  10851  dedekindle  11280  divgt0  11993  divge0  11994  nnne0  12162  uzind  12568  uzind2  12569  iccsplit  13388  ssnn0fi  13892  expmordi  14074  sqlecan  14116  modexp  14145  expnngt1  14148  facavg  14208  2cshwcshw  14732  relexpcnv  14942  relexpaddnn  14958  relexpaddg  14960  pwdif  15775  prodfn0  15801  prodfrec  15802  ntrivcvgfvn0  15806  fprodabs  15881  bpolycl  15959  bpolydif  15962  fprodefsum  16002  dvdsmodexp  16171  dvdsaddre2b  16218  nn0rppwr  16472  dvdsnprmd  16601  2mulprm  16604  prmndvdsfaclt  16636  ncoprmlnprm  16639  fermltl  16695  pceu  16758  setsstruct2  17085  setsstruct  17087  mreexexd  17554  isglbd  18415  symgpssefmnd  19275  pmtrfrn  19337  psgnunilem4  19376  ablsimpgprmd  19996  mulgass2  20194  islss4  20865  lspsneu  21030  lspfixed  21035  lspexch  21036  lsmcv  21048  lspsolvlem  21049  rnglidlmcl  21123  xrsdsreclblem  21319  nzerooringczr  21387  isphld  21561  mdetralt  22493  mdetunilem9  22505  fiinopn  22786  neips  22998  tpnei  23006  neindisj2  23008  opnneiid  23011  hausnei2  23238  cmpsublem  23284  cmpsub  23285  cmpcld  23287  comppfsc  23417  filufint  23805  cfinufil  23813  rnelfm  23838  alexsubALTlem1  23932  alexsubALTlem4  23935  alexsubALT  23936  tsmsxp  24040  neibl  24387  tngngp3  24542  tgqioo  24686  ovolunlem2  25397  iunmbl2  25456  itg1le  25612  vieta1  26218  aannenlem2  26235  aalioulem3  26240  aalioulem4  26241  aaliou2  26246  wilthlem3  26978  bcmono  27186  gausslemma2dlem1a  27274  sslttr  27718  ssltun1  27719  ssltun2  27720  sltlpss  27822  precsexlem8  28121  precsexlem9  28122  precsex  28125  onsfi  28252  expscllem  28322  expsgt0  28329  pw2cut  28348  iscgrglt  28459  axcontlem7  28915  elntg2  28930  edglnl  29088  numedglnl  29089  ausgrumgri  29112  ausgrusgri  29113  usgrausgrb  29114  usgredg2vtxeuALT  29167  ushgredgedg  29174  ushgredgedgloop  29176  nbuhgr2vtx1edgb  29297  cusgrsize2inds  29399  upgrewlkle2  29552  wlkl1loop  29583  redwlk  29616  pthdivtx  29672  pthdadjvtx  29673  upgr2pthnlp  29677  upgrspthswlk  29683  clwlkl1loop  29728  cyclnumvtx  29745  wwlksnred  29837  wwlksnextbi  29839  elwwlks2ons3im  29899  umgrwwlks2on  29902  clwwlknwwlksn  29982  clwwlkinwwlk  29984  wwlksext2clwwlk  30001  1pthon2v  30097  uhgr3cyclex  30126  n4cyclfrgr  30235  frgrwopreg  30267  numclwwlk1lem2f1  30301  clwwlknonclwlknonf1o  30306  wlkl0  30311  frgrreggt1  30337  frgrreg  30338  frgrregord013  30339  chintcli  31275  spansnss  31515  elspansn4  31517  chscllem4  31584  hoadddir  31748  adjmul  32036  kbass6  32065  spansncv2  32237  sumdmdii  32359  nexple  32789  bnj1417  35008  lfuhgr2  35092  cusgredgex  35095  sat1el2xp  35352  fmlasuc  35359  satffunlem1lem1  35375  satffunlem2lem1  35377  mclsind  35543  iprodefisumlem  35713  btwndiff  36001  elicc3  36291  finminlem  36292  sdclem2  37722  clmgmOLD  37831  grpomndo  37855  zerdivemp1x  37927  lsmsat  38987  lsmcv2  39008  lcvat  39009  lsatcveq0  39011  lcvexchlem4  39016  lcvexchlem5  39017  islshpcv  39032  l1cvpat  39033  lshpkrlem6  39094  omlfh3N  39238  cvlsupr4  39324  cvlsupr5  39325  cvlsupr6  39326  2llnneN  39388  hlrelat3  39391  cvrval3  39392  cvrval4N  39393  cvrexchlem  39398  2atlt  39418  cvrat4  39422  atbtwnexOLDN  39426  atbtwnex  39427  athgt  39435  3dim1  39446  3dim2  39447  3dim3  39448  1cvratex  39452  llnle  39497  atcvrlln2  39498  atcvrlln  39499  2llnmat  39503  lplnle  39519  lplnnle2at  39520  lplnnlelln  39522  llncvrlpln2  39536  2llnjN  39546  lvoli2  39560  lvolnlelln  39563  lvolnlelpln  39564  4atlem10  39585  4atlem11  39588  4atlem12  39591  lplncvrlvol2  39594  2lplnj  39599  lneq2at  39757  lnatexN  39758  lnjatN  39759  lncvrat  39761  2lnat  39763  cdlemb  39773  paddasslem14  39812  llnexchb2  39848  dalawlem10  39859  dalawlem13  39862  dalawlem14  39863  dalaw  39865  pclclN  39870  pclfinN  39879  osumcllem11N  39945  lhp2lt  39980  lhpexle3lem  39990  4atexlem7  40054  ldilcnv  40094  ldilco  40095  ltrncnv  40125  trlval2  40142  cdleme24  40331  cdleme26ee  40339  cdleme28  40352  cdleme32le  40426  cdleme50trn2  40530  cdleme50ltrn  40536  cdleme  40539  cdlemf1  40540  cdlemf  40542  cdlemg1cex  40567  cdlemg2ce  40571  cdlemg18b  40658  ltrnco  40698  tendocan  40803  cdlemk28-3  40887  cdlemk11t  40925  dia2dimlem6  41048  dia2dimlem12  41054  dihlsscpre  41213  dihord4  41237  dihord5b  41238  dihmeetlem3N  41284  dihmeetlem20N  41305  dvh4dimlem  41422  lclkrlem2y  41510  mapdpglem24  41683  mapdpglem32  41684  mapdpg  41685  baerlem3lem2  41689  baerlem5alem2  41690  baerlem5blem2  41691  mapdh9a  41768  mapdh9aOLDN  41769  hdmap14lem6  41852  hdmapglem7  41908  indstrd  42166  nnadddir  42243  nnmulcom  42245  sn-addlid  42377  remulcand  42412  mzpexpmpt  42718  pellexlem5  42806  pellex  42808  pell14qrexpclnn0  42839  pellfundex  42859  monotuz  42914  monotoddzzfi  42915  rmxypos  42920  jm2.17a  42933  jm2.17b  42934  rmygeid  42937  jm2.19lem3  42964  jm2.15nn0  42976  jm2.16nn0  42977  aomclem2  43028  aomclem6  43032  dfac11  43035  hbtlem5  43101  cnsrexpcl  43138  cantnf2  43298  dflim5  43302  relexpxpnnidm  43676  relexpiidm  43677  relexpss1d  43678  iunrelexpmin1  43681  relexpmulnn  43682  iunrelexpmin2  43685  relexp01min  43686  relexp0a  43689  relexpxpmin  43690  relexpaddss  43691  trclimalb2  43699  tfindsd  44183  3impexpbicomi  44455  ee333  44481  eel12131  44686  eel2122old  44691  e333  44706  ordelordALTVD  44840  refsumcn  45008  uzwo4  45031  ssinc  45065  ssdec  45066  iunincfi  45072  restuni3  45096  eliuniin2  45098  rabssd  45120  reximdd  45126  suprnmpt  45152  disjf1o  45169  disjinfi  45170  ssnnf1octb  45172  choicefi  45178  mapssbi  45191  unirnmapsn  45192  iunmapsn  45195  rnmptlb  45221  rnmptbddlem  45222  infnsuprnmpt  45228  fperiodmullem  45285  upbdrech  45287  ssfiunibd  45291  supxrgere  45313  iuneqfzuzlem  45314  supxrgelem  45317  supxrge  45318  suplesup  45319  infrpge  45331  infleinf  45351  suplesup2  45355  supxrunb3  45378  infleinf2  45393  rexabslelem  45397  infrnmptle  45402  infxrunb3rnmpt  45407  iccshift  45499  iooshift  45503  fmul01  45561  fmuldfeq  45564  fmul01lt1  45567  mullimc  45597  islptre  45600  mullimcf  45604  limcperiod  45609  islpcn  45620  limsupre  45622  limcleqr  45625  neglimc  45628  addlimc  45629  0ellimcdiv  45630  limclner  45632  fnlimfvre  45655  limsuppnflem  45691  limsupmnfuzlem  45707  limsupre3lem  45713  limsupre3uzlem  45716  climuzlem  45724  limsupgtlem  45758  coskpi2  45847  cosknegpi  45850  cncfshift  45855  cncfperiod  45860  icccncfext  45868  dvnmptdivc  45919  dvnmptconst  45922  dvnmul  45924  dvmptfprodlem  45925  dvmptfprod  45926  dvnprodlem1  45927  dvnprodlem2  45928  iblspltprt  45954  itgspltprt  45960  itgperiod  45962  ismbl3  45967  stoweidlem3  45984  stoweidlem31  46012  stoweidlem59  46040  stirlinglem13  46067  fourierdlem41  46129  fourierdlem42  46130  fourierdlem48  46135  fourierdlem51  46138  fourierdlem70  46157  fourierdlem71  46158  fourierdlem73  46160  fourierdlem80  46167  fourierdlem81  46168  fourierdlem89  46176  fourierdlem91  46178  fourierdlem93  46180  fourierdlem97  46184  elaa2  46215  qndenserrnopnlem  46278  salexct  46315  subsaliuncl  46339  subsalsal  46340  sge0tsms  46361  sge0f1o  46363  sge0fsum  46368  sge0supre  46370  sge0sup  46372  sge0rnbnd  46374  sge0gerp  46376  sge0pnffigt  46377  sge0lefi  46379  sge0ltfirp  46381  sge0resrn  46385  sge0resplit  46387  sge0split  46390  sge0iunmptlemfi  46394  sge0iunmptlemre  46396  sge0iunmpt  46399  sge0rpcpnf  46402  sge0isum  46408  sge0xp  46410  sge0xaddlem2  46415  sge0uzfsumgt  46425  sge0seq  46427  sge0reuz  46428  nnfoctbdjlem  46436  nnfoctbdj  46437  iundjiun  46441  meadjiunlem  46446  voliunsge0lem  46453  meaiuninclem  46461  meaiininc2  46469  carageniuncllem1  46502  carageniuncllem2  46503  caratheodorylem1  46507  caratheodorylem2  46508  isomenndlem  46511  ovnsupge0  46538  ovnlerp  46543  ovncvrrp  46545  ovnsubaddlem1  46551  hoidmvval0  46568  hoidmv1lelem3  46574  hoidmv1le  46575  hoidmvlelem1  46576  hoidmvlelem2  46577  hoidmvlelem3  46578  ovnhoilem2  46583  opnvonmbllem2  46614  ovnovollem3  46639  vonioo  46663  vonicc  46666  pimiooltgt  46691  sssmf  46719  smfaddlem1  46744  smflimlem6  46757  smfmullem4  46775  smfpimbor1lem1  46779  smfco  46783  smfpimcc  46789  smflimmpt  46791  smfinflem  46798  smflimsuplem7  46807  smflimsuplem8  46808  smflimsupmpt  46810  smfliminfmpt  46813  cfsetsnfsetf1  47043  2tceilhalfelfzo1  47316  elsetpreimafveqfv  47376  iccpartiltu  47406  sprsymrelfvlem  47474  reuopreuprim  47510  goldbachth  47531  fmtnofac1  47554  prmdvdsfmtnof1lem1  47568  lighneal  47595  grimuhgr  47871  uhgrimedgi  47874  uhgrimisgrgriclem  47914  clnbgrgrim  47918  grimedg  47919  usgrgrtrirex  47934  isubgr3stgrlem3  47952  isubgr3stgrlem6  47955  uspgrlimlem2  47973  grlimgrtri  47987  grlicsym  47997  clnbgr3stgrgrlic  48004  gpgusgralem  48040  gpgedgvtx1  48046  gpgvtxedg0  48047  gpgvtxedg1  48048  uspgropssxp  48128  rngccatidALTV  48256  ringccatidALTV  48290  lcosslsp  48423  fllog2  48553  dignn0flhalf  48603  fv1arycl  48622  1arymaptf1  48627  fv2arycl  48633  2arymaptf1  48638  itschlc0yqe  48745  itsclc0xyqsol  48753  seposep  48910  iscnrm3lem6  48922  iunord  49661  setrec2fun  49677