Theorem 3exp 1137

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3expb  1138  3expib  1140  3com12  1141  3com13  1142  pm3.2an3  1359  3exp1  1371  3expd  1372  exp5o  1374  3ecase  1505  rexlimdv3a  3167  rabssdv  3999  reupick2  4276  disjiund  5093  otiunsndisj  5492  wefrc  5644  tz7.7  6388  unizlim  6487  funimassd  6951  fvelimad  6952  fveqdmss  7078  fompt  7118  f1resrcmplf1d  7279  f1oiso2  7360  ssorduni  7793  tfisi  7870  resf1extb  7946  funeldmdif  8059  poxp  8140  poseq  8175  fpr3g  8303  frrlem10  8313  smo11  8372  tfrlem5  8387  odi  8587  omass  8588  nndi  8632  nnmass  8633  naddoa  8712  undifixp  8962  findcard  9179  php3  9224  ac6sfi  9275  domunfican  9313  mapfien2  9401  fisup2g  9461  fiinf2g  9494  ttrclss  9721  ttrclselem2  9727  setrec2fun  9973  indcardi  10120  acndom  10130  ackbij1lem16  10312  infpssrlem4  10384  fin23lem11  10395  isfin2-2  10397  fin23lem34  10424  fin1a2lem10  10487  hsmexlem2  10505  axcc3  10516  domtriomlem  10520  axdc3lem2  10529  axdc3lem4  10531  axcclem  10535  ttukeyg  10595  axdclem2  10598  axacndlem4  10695  axacndlem5  10696  axacnd  10697  tskhf  10853  tskwe2  10858  tskord  10865  tskcard  10866  tskuni  10868  tskwun  10869  gruiin  10895  grudomon  10902  gruina  10903  mulcanpi  10985  adderpq  11041  mulerpq  11042  dedekindle  11474  divgt0  12185  divge0  12186  nnne0  12372  nnadddir  12394  nnmulcom  12396  uzind  12791  uzind2  12792  iccsplit  13616  ssnn0fi  14128  expmordi  14310  sqlecan  14353  modexp  14382  expnngt1  14385  facavg  14445  2cshwcshw  14976  relexpcnv  15188  relexpaddnn  15204  relexpaddg  15206  pwdif  16037  prodfn0  16063  prodfrec  16064  ntrivcvgfvn0  16068  fprodabs  16141  bpolycl  16218  bpolydif  16221  fprodefsum  16261  dvdsmodexp  16430  dvdsaddre2b  16477  nn0rppwr  16735  dvdsnprmd  16865  2mulprm  16868  prmndvdsfaclt  16901  ncoprmlnprm  16904  fermltl  16961  pceu  17024  setsstruct2  17352  setsstruct  17354  mreexexd  17822  isglbd  18683  symgpssefmnd  19610  pmtrfrn  19672  psgnunilem4  19711  ablsimpgprmd  20331  mulgass2  20540  islss4  21237  lspsneu  21401  lspfixed  21406  lspexch  21407  lsmcv  21419  lspsolvlem  21420  rnglidlmcl  21495  unichnlidl  21516  xrsdsreclblem  21719  nzerooringczr  21786  isphld  21960  mdetralt  22923  mdetunilem9  22935  fiinopn  23219  neips  23431  tpnei  23439  neindisj2  23441  opnneiid  23444  hausnei2  23671  cmpsublem  23717  cmpsub  23718  cmpcld  23720  comppfsc  23851  filufint  24239  cfinufil  24247  rnelfm  24272  alexsubALTlem1  24366  alexsubALTlem4  24369  alexsubALT  24370  tsmsxp  24474  neibl  24820  tngngp3  24975  tgqioo  25119  ovolunlem2  25819  iunmbl2  25878  itg1le  26034  vieta1  26635  aannenlem2  26656  aalioulem3  26661  aalioulem4  26662  aaliou2  26667  wilthlem3  27397  bcmono  27604  gausslemma2dlem1a  27692  sltstr  28173  sltsun1  28174  sltsun2  28175  ltslpss  28294  precsexlem8  28600  precsexlem9  28601  precsex  28604  onsfi  28742  oldfib  28763  expscllem  28816  expsgt0  28823  pw2cut  28846  pw2cut2  28848  bdaypw2n0bnd  28850  bdayfin  28873  iscgrglt  28977  axcontlem7  29548  elntg2  29563  edglnl  29721  numedglnl  29722  lfuhgr2  29727  ausgrumgri  29748  ausgrusgri  29749  usgrausgrb  29750  usgredg2vtxeuALT  29803  ushgredgedg  29810  ushgredgedgloop  29812  nbuhgr2vtx1edgb  29933  cusgrsize2inds  30034  upgrewlkle2  30187  wlkl1loop  30218  redwlk  30251  pthdivtx  30312  pthdadjvtx  30313  upgr2pthnlp  30318  upgrspthswlk  30324  clwlkl1loop  30370  cyclnumvtx  30388  wwlksnred  30481  wwlksnextbi  30483  elwwlks2ons3im  30543  usgrwwlks2on  30547  umgrwwlks2on  30548  clwwlknwwlksn  30629  clwwlkinwwlk  30631  wwlksext2clwwlk  30648  1pthon2v  30754  uhgr3cyclex  30783  n4cyclfrgr  30892  frgrwopreg  30924  numclwwlk1lem2f1  30958  clwwlknonclwlknonf1o  30963  wlkl0  30968  frgrreggt1  30994  frgrreg  30995  frgrregord013  30996  chintcli  31933  spansnss  32173  elspansn4  32175  chscllem4  32242  hoadddir  32406  adjmul  32694  kbass6  32723  spansncv2  32895  sumdmdii  33017  nexple  33424  bnj1417  35671  cusgredgex  35906  sat1el2xp  36144  fmlasuc  36151  satffunlem1lem1  36167  satffunlem2lem1  36169  mclsind  36335  iprodefisumlem  36505  btwndiff  36792  elicc3  37105  finminlem  37106  axtcond  37266  ttcmin  37284  sdclem2  38677  clmgmOLD  38786  grpomndo  38810  zerdivemp1x  38882  lsmsat  40066  lsmcv2  40087  lcvat  40088  lsatcveq0  40090  lcvexchlem4  40095  lcvexchlem5  40096  islshpcv  40111  l1cvpat  40112  lshpkrlem6  40173  omlfh3N  40317  cvlsupr4  40403  cvlsupr5  40404  cvlsupr6  40405  2llnneN  40467  hlrelat3  40470  cvrval3  40471  cvrval4N  40472  cvrexchlem  40477  2atlt  40497  cvrat4  40501  atbtwnexOLDN  40505  atbtwnex  40506  athgt  40514  3dim1  40525  3dim2  40526  3dim3  40527  1cvratex  40531  llnle  40576  atcvrlln2  40577  atcvrlln  40578  2llnmat  40582  lplnle  40598  lplnnle2at  40599  lplnnlelln  40601  llncvrlpln2  40615  2llnjN  40625  lvoli2  40639  lvolnlelln  40642  lvolnlelpln  40643  4atlem10  40664  4atlem11  40667  4atlem12  40670  lplncvrlvol2  40673  2lplnj  40678  lneq2at  40836  lnatexN  40837  lnjatN  40838  lncvrat  40840  2lnat  40842  cdlemb  40852  paddasslem14  40891  llnexchb2  40927  dalawlem10  40938  dalawlem13  40941  dalawlem14  40942  dalaw  40944  pclclN  40949  pclfinN  40958  osumcllem11N  41024  lhp2lt  41059  lhpexle3lem  41069  4atexlem7  41133  ldilcnv  41173  ldilco  41174  ltrncnv  41204  trlval2  41221  cdleme24  41410  cdleme26ee  41418  cdleme28  41431  cdleme32le  41505  cdleme50trn2  41609  cdleme50ltrn  41615  cdleme  41618  cdlemf1  41619  cdlemf  41621  cdlemg1cex  41646  cdlemg2ce  41650  cdlemg18b  41737  ltrnco  41777  tendocan  41882  cdlemk28-3  41966  cdlemk11t  42004  dia2dimlem6  42127  dia2dimlem12  42133  dihlsscpre  42292  dihord4  42316  dihord5b  42317  dihmeetlem3N  42363  dihmeetlem20N  42384  dvh4dimlem  42501  lclkrlem2y  42589  mapdpglem24  42762  mapdpglem32  42763  mapdpg  42764  baerlem3lem2  42768  baerlem5alem2  42769  baerlem5blem2  42770  mapdh9a  42847  mapdh9aOLDN  42848  hdmap14lem6  42931  hdmapglem7  42987  indstrd  43244  sn-addlid  43456  remulcand  43491  mzpexpmpt  43756  pellexlem5  43840  pellex  43842  pell14qrexpclnn0  43873  pellfundex  43893  monotuz  43948  monotoddzzfi  43949  rmxypos  43954  jm2.17a  43967  jm2.17b  43968  rmygeid  43971  jm2.19lem3  43998  jm2.15nn0  44010  jm2.16nn0  44011  aomclem2  44057  aomclem6  44061  dfac11  44064  hbtlem5  44130  cnsrexpcl  44167  cantnf2  44327  dflim5  44331  relexpxpnnidm  44703  relexpiidm  44704  relexpss1d  44705  iunrelexpmin1  44708  relexpmulnn  44709  iunrelexpmin2  44712  relexp01min  44713  relexp0a  44716  relexpxpmin  44717  relexpaddss  44718  trclimalb2  44726  tfindsd  45208  3impexpbicomi  45464  ee333  45490  eel12131  45695  eel2122old  45700  e333  45715  ordelordALTVD  45849  refsumcn  46047  uzwo4  46070  ssinc  46102  ssdec  46103  iunincfi  46109  restuni3  46133  eliuniin2  46135  rabssd  46157  reximdd  46163  suprnmpt  46189  disjf1o  46206  disjinfi  46207  ssnnf1octb  46209  choicefi  46214  mapssbi  46226  unirnmapsn  46227  iunmapsn  46230  rnmptlb  46255  rnmptbddlem  46256  infnsuprnmpt  46262  fperiodmullem  46319  upbdrech  46321  ssfiunibd  46325  supxrgere  46345  iuneqfzuzlem  46346  supxrgelem  46349  supxrge  46350  suplesup  46351  infrpge  46363  infleinf  46383  suplesup2  46387  supxrunb3  46410  infleinf2  46424  rexabslelem  46428  infrnmptle  46433  infxrunb3rnmpt  46438  iccshift  46530  iooshift  46534  fmul01  46592  fmuldfeq  46595  fmul01lt1  46598  mullimc  46628  islptre  46631  mullimcf  46635  limcperiod  46640  islpcn  46649  limsupre  46651  limcleqr  46654  neglimc  46657  addlimc  46658  0ellimcdiv  46659  limclner  46661  fnlimfvre  46684  limsuppnflem  46720  limsupmnfuzlem  46736  limsupre3lem  46742  limsupre3uzlem  46745  climuzlem  46753  limsupgtlem  46787  coskpi2  46876  cosknegpi  46879  cncfshift  46884  cncfperiod  46889  icccncfext  46897  dvnmptdivc  46948  dvnmptconst  46951  dvnmul  46953  dvmptfprodlem  46954  dvmptfprod  46955  dvnprodlem1  46956  dvnprodlem2  46957  iblspltprt  46983  itgspltprt  46989  itgperiod  46991  ismbl3  46996  stoweidlem3  47013  stoweidlem31  47041  stoweidlem59  47069  stirlinglem13  47096  fourierdlem41  47158  fourierdlem42  47159  fourierdlem48  47164  fourierdlem51  47167  fourierdlem70  47186  fourierdlem71  47187  fourierdlem73  47189  fourierdlem80  47196  fourierdlem81  47197  fourierdlem89  47205  fourierdlem91  47207  fourierdlem93  47209  fourierdlem97  47213  elaa2  47244  qndenserrnopnlem  47307  salexct  47344  subsaliuncl  47368  subsalsal  47369  sge0tsms  47390  sge0f1o  47392  sge0fsum  47397  sge0supre  47399  sge0sup  47401  sge0rnbnd  47403  sge0gerp  47405  sge0pnffigt  47406  sge0lefi  47408  sge0ltfirp  47410  sge0resrn  47414  sge0resplit  47416  sge0split  47419  sge0iunmptlemfi  47423  sge0iunmptlemre  47425  sge0iunmpt  47428  sge0rpcpnf  47431  sge0isum  47437  sge0xp  47439  sge0xaddlem2  47444  sge0uzfsumgt  47454  sge0seq  47456  sge0reuz  47457  nnfoctbdjlem  47465  nnfoctbdj  47466  iundjiun  47470  meadjiunlem  47475  voliunsge0lem  47482  meaiuninclem  47490  meaiininc2  47498  carageniuncllem1  47531  carageniuncllem2  47532  caratheodorylem1  47536  caratheodorylem2  47537  isomenndlem  47540  ovnsupge0  47567  ovnlerp  47572  ovncvrrp  47574  ovnsubaddlem1  47580  hoidmvval0  47597  hoidmv1lelem3  47603  hoidmv1le  47604  hoidmvlelem1  47605  hoidmvlelem2  47606  hoidmvlelem3  47607  ovnhoilem2  47612  opnvonmbllem2  47643  ovnovollem3  47668  vonioo  47692  vonicc  47695  pimiooltgt  47720  smfaddlem1  47773  smflimlem6  47786  smfmullem4  47804  smfpimbor1lem1  47808  smfco  47812  smfpimcc  47818  smflimmpt  47820  smfinflem  47827  smflimsuplem7  47836  smflimsuplem8  47837  smflimsupmpt  47839  smfliminfmpt  47842  cfsetsnfsetf1  48129  nnmul2b  48401  2tceilhalfelfzo1  48406  elsetpreimafveqfv  48474  iccpartiltu  48504  sprsymrelfvlem  48572  reuopreuprim  48608  nprmmul2  48610  goldbachth  48632  fmtnofac1  48655  prmdvdsfmtnof1lem1  48669  lighneal  48696  grimuhgr  48985  uhgrimedgi  48988  uhgrimisgrgriclem  49028  clnbgrgrim  49032  grimedg  49033  usgrgrtrirex  49048  isubgr3stgrlem3  49066  isubgr3stgrlem6  49069  uspgrlimlem2  49087  grlimgrtri  49101  grlicsym  49111  clnbgr3stgrgrlic  49118  gpgusgralem  49154  gpgedgvtx1  49160  gpgvtxedg0  49161  gpgvtxedg1  49162  uspgropssxp  49242  rngccatidALTV  49369  ringccatidALTV  49403  lcosslsp  49550  fllog2  49680  dignn0flhalf  49730  fv1arycl  49749  1arymaptf1  49754  fv2arycl  49760  2arymaptf1  49765  itschlc0yqe  49872  itsclc0xyqsol  49880  seposep  50034  iscnrm3lem6  50046  iunord  50784