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  3168  rabssdv  4022  reupick2  4277  disjiund  5094  otiunsndisj  5493  wefrc  5645  tz7.7  6387  unizlim  6486  funimassd  6949  fvelimad  6950  fveqdmss  7076  fompt  7116  f1resrcmplf1d  7277  f1oiso2  7358  ssorduni  7791  tfisi  7868  resf1extb  7944  funeldmdif  8057  poxp  8138  poseq  8168  fpr3g  8296  frrlem10  8306  smo11  8365  tfrlem5  8380  odi  8580  omass  8581  nndi  8625  nnmass  8626  naddoa  8705  undifixp  8955  findcard  9172  php3  9217  ac6sfi  9268  domunfican  9306  mapfien2  9394  fisup2g  9454  fiinf2g  9487  ttrclss  9714  ttrclselem2  9720  setrec2fun  9966  indcardi  10113  acndom  10123  ackbij1lem16  10305  infpssrlem4  10377  fin23lem11  10388  isfin2-2  10390  fin23lem34  10417  fin1a2lem10  10480  hsmexlem2  10498  axcc3  10509  domtriomlem  10513  axdc3lem2  10522  axdc3lem4  10524  axcclem  10528  ttukeyg  10588  axdclem2  10591  axacndlem4  10688  axacndlem5  10689  axacnd  10690  tskhf  10846  tskwe2  10851  tskord  10858  tskcard  10859  tskuni  10861  tskwun  10862  gruiin  10888  grudomon  10895  gruina  10896  mulcanpi  10978  adderpq  11034  mulerpq  11035  dedekindle  11467  divgt0  12178  divge0  12179  nnne0  12365  nnadddir  12387  nnmulcom  12389  uzind  12784  uzind2  12785  iccsplit  13609  ssnn0fi  14121  expmordi  14303  sqlecan  14346  modexp  14375  expnngt1  14378  facavg  14438  2cshwcshw  14969  relexpcnv  15181  relexpaddnn  15197  relexpaddg  15199  pwdif  16030  prodfn0  16056  prodfrec  16057  ntrivcvgfvn0  16061  fprodabs  16134  bpolycl  16211  bpolydif  16214  fprodefsum  16254  dvdsmodexp  16423  dvdsaddre2b  16470  nn0rppwr  16728  dvdsnprmd  16858  2mulprm  16861  prmndvdsfaclt  16894  ncoprmlnprm  16897  fermltl  16954  pceu  17017  setsstruct2  17345  setsstruct  17347  mreexexd  17815  isglbd  18676  symgpssefmnd  19603  pmtrfrn  19665  psgnunilem4  19704  ablsimpgprmd  20324  mulgass2  20533  islss4  21230  lspsneu  21394  lspfixed  21399  lspexch  21400  lsmcv  21412  lspsolvlem  21413  rnglidlmcl  21488  unichnlidl  21509  xrsdsreclblem  21712  nzerooringczr  21779  isphld  21953  mdetralt  22916  mdetunilem9  22928  fiinopn  23212  neips  23424  tpnei  23432  neindisj2  23434  opnneiid  23437  hausnei2  23664  cmpsublem  23710  cmpsub  23711  cmpcld  23713  comppfsc  23844  filufint  24232  cfinufil  24240  rnelfm  24265  alexsubALTlem1  24359  alexsubALTlem4  24362  alexsubALT  24363  tsmsxp  24467  neibl  24813  tngngp3  24968  tgqioo  25112  ovolunlem2  25812  iunmbl2  25871  itg1le  26027  vieta1  26628  aannenlem2  26649  aalioulem3  26654  aalioulem4  26655  aaliou2  26660  wilthlem3  27390  bcmono  27597  gausslemma2dlem1a  27685  sltstr  28166  sltsun1  28167  sltsun2  28168  ltslpss  28287  precsexlem8  28593  precsexlem9  28594  precsex  28597  onsfi  28735  oldfib  28756  expscllem  28809  expsgt0  28816  pw2cut  28839  pw2cut2  28841  bdaypw2n0bnd  28843  bdayfin  28866  iscgrglt  28970  axcontlem7  29541  elntg2  29556  edglnl  29714  numedglnl  29715  lfuhgr2  29720  ausgrumgri  29741  ausgrusgri  29742  usgrausgrb  29743  usgredg2vtxeuALT  29796  ushgredgedg  29803  ushgredgedgloop  29805  nbuhgr2vtx1edgb  29926  cusgrsize2inds  30027  upgrewlkle2  30180  wlkl1loop  30211  redwlk  30244  pthdivtx  30305  pthdadjvtx  30306  upgr2pthnlp  30311  upgrspthswlk  30317  clwlkl1loop  30363  cyclnumvtx  30381  wwlksnred  30474  wwlksnextbi  30476  elwwlks2ons3im  30536  usgrwwlks2on  30540  umgrwwlks2on  30541  clwwlknwwlksn  30622  clwwlkinwwlk  30624  wwlksext2clwwlk  30641  1pthon2v  30747  uhgr3cyclex  30776  n4cyclfrgr  30885  frgrwopreg  30917  numclwwlk1lem2f1  30951  clwwlknonclwlknonf1o  30956  wlkl0  30961  frgrreggt1  30987  frgrreg  30988  frgrregord013  30989  chintcli  31926  spansnss  32166  elspansn4  32168  chscllem4  32235  hoadddir  32399  adjmul  32687  kbass6  32716  spansncv2  32888  sumdmdii  33010  nexple  33417  bnj1417  35664  cusgredgex  35885  sat1el2xp  36123  fmlasuc  36130  satffunlem1lem1  36146  satffunlem2lem1  36148  mclsind  36314  iprodefisumlem  36484  btwndiff  36772  elicc3  37085  finminlem  37086  axtcond  37246  ttcmin  37264  sdclem2  38656  clmgmOLD  38765  grpomndo  38789  zerdivemp1x  38861  lsmsat  40045  lsmcv2  40066  lcvat  40067  lsatcveq0  40069  lcvexchlem4  40074  lcvexchlem5  40075  islshpcv  40090  l1cvpat  40091  lshpkrlem6  40152  omlfh3N  40296  cvlsupr4  40382  cvlsupr5  40383  cvlsupr6  40384  2llnneN  40446  hlrelat3  40449  cvrval3  40450  cvrval4N  40451  cvrexchlem  40456  2atlt  40476  cvrat4  40480  atbtwnexOLDN  40484  atbtwnex  40485  athgt  40493  3dim1  40504  3dim2  40505  3dim3  40506  1cvratex  40510  llnle  40555  atcvrlln2  40556  atcvrlln  40557  2llnmat  40561  lplnle  40577  lplnnle2at  40578  lplnnlelln  40580  llncvrlpln2  40594  2llnjN  40604  lvoli2  40618  lvolnlelln  40621  lvolnlelpln  40622  4atlem10  40643  4atlem11  40646  4atlem12  40649  lplncvrlvol2  40652  2lplnj  40657  lneq2at  40815  lnatexN  40816  lnjatN  40817  lncvrat  40819  2lnat  40821  cdlemb  40831  paddasslem14  40870  llnexchb2  40906  dalawlem10  40917  dalawlem13  40920  dalawlem14  40921  dalaw  40923  pclclN  40928  pclfinN  40937  osumcllem11N  41003  lhp2lt  41038  lhpexle3lem  41048  4atexlem7  41112  ldilcnv  41152  ldilco  41153  ltrncnv  41183  trlval2  41200  cdleme24  41389  cdleme26ee  41397  cdleme28  41410  cdleme32le  41484  cdleme50trn2  41588  cdleme50ltrn  41594  cdleme  41597  cdlemf1  41598  cdlemf  41600  cdlemg1cex  41625  cdlemg2ce  41629  cdlemg18b  41716  ltrnco  41756  tendocan  41861  cdlemk28-3  41945  cdlemk11t  41983  dia2dimlem6  42106  dia2dimlem12  42112  dihlsscpre  42271  dihord4  42295  dihord5b  42296  dihmeetlem3N  42342  dihmeetlem20N  42363  dvh4dimlem  42480  lclkrlem2y  42568  mapdpglem24  42741  mapdpglem32  42742  mapdpg  42743  baerlem3lem2  42747  baerlem5alem2  42748  baerlem5blem2  42749  mapdh9a  42826  mapdh9aOLDN  42827  hdmap14lem6  42910  hdmapglem7  42966  indstrd  43223  sn-addlid  43435  remulcand  43470  mzpexpmpt  43735  pellexlem5  43819  pellex  43821  pell14qrexpclnn0  43852  pellfundex  43872  monotuz  43927  monotoddzzfi  43928  rmxypos  43933  jm2.17a  43946  jm2.17b  43947  rmygeid  43950  jm2.19lem3  43977  jm2.15nn0  43989  jm2.16nn0  43990  aomclem2  44041  aomclem6  44045  dfac11  44048  hbtlem5  44114  cnsrexpcl  44151  cantnf2  44311  dflim5  44315  relexpxpnnidm  44688  relexpiidm  44689  relexpss1d  44690  iunrelexpmin1  44693  relexpmulnn  44694  iunrelexpmin2  44697  relexp01min  44698  relexp0a  44701  relexpxpmin  44702  relexpaddss  44703  trclimalb2  44711  tfindsd  45193  3impexpbicomi  45449  ee333  45475  eel12131  45680  eel2122old  45685  e333  45700  ordelordALTVD  45834  refsumcn  46016  uzwo4  46039  ssinc  46071  ssdec  46072  iunincfi  46078  restuni3  46102  eliuniin2  46104  rabssd  46126  reximdd  46132  suprnmpt  46158  disjf1o  46175  disjinfi  46176  ssnnf1octb  46178  choicefi  46183  mapssbi  46195  unirnmapsn  46196  iunmapsn  46199  rnmptlb  46224  rnmptbddlem  46225  infnsuprnmpt  46231  fperiodmullem  46288  upbdrech  46290  ssfiunibd  46294  supxrgere  46314  iuneqfzuzlem  46315  supxrgelem  46318  supxrge  46319  suplesup  46320  infrpge  46332  infleinf  46352  suplesup2  46356  supxrunb3  46379  infleinf2  46393  rexabslelem  46397  infrnmptle  46402  infxrunb3rnmpt  46407  iccshift  46499  iooshift  46503  fmul01  46561  fmuldfeq  46564  fmul01lt1  46567  mullimc  46597  islptre  46600  mullimcf  46604  limcperiod  46609  islpcn  46618  limsupre  46620  limcleqr  46623  neglimc  46626  addlimc  46627  0ellimcdiv  46628  limclner  46630  fnlimfvre  46653  limsuppnflem  46689  limsupmnfuzlem  46705  limsupre3lem  46711  limsupre3uzlem  46714  climuzlem  46722  limsupgtlem  46756  coskpi2  46845  cosknegpi  46848  cncfshift  46853  cncfperiod  46858  icccncfext  46866  dvnmptdivc  46917  dvnmptconst  46920  dvnmul  46922  dvmptfprodlem  46923  dvmptfprod  46924  dvnprodlem1  46925  dvnprodlem2  46926  iblspltprt  46952  itgspltprt  46958  itgperiod  46960  ismbl3  46965  stoweidlem3  46982  stoweidlem31  47010  stoweidlem59  47038  stirlinglem13  47065  fourierdlem41  47127  fourierdlem42  47128  fourierdlem48  47133  fourierdlem51  47136  fourierdlem70  47155  fourierdlem71  47156  fourierdlem73  47158  fourierdlem80  47165  fourierdlem81  47166  fourierdlem89  47174  fourierdlem91  47176  fourierdlem93  47178  fourierdlem97  47182  elaa2  47213  qndenserrnopnlem  47276  salexct  47313  subsaliuncl  47337  subsalsal  47338  sge0tsms  47359  sge0f1o  47361  sge0fsum  47366  sge0supre  47368  sge0sup  47370  sge0rnbnd  47372  sge0gerp  47374  sge0pnffigt  47375  sge0lefi  47377  sge0ltfirp  47379  sge0resrn  47383  sge0resplit  47385  sge0split  47388  sge0iunmptlemfi  47392  sge0iunmptlemre  47394  sge0iunmpt  47397  sge0rpcpnf  47400  sge0isum  47406  sge0xp  47408  sge0xaddlem2  47413  sge0uzfsumgt  47423  sge0seq  47425  sge0reuz  47426  nnfoctbdjlem  47434  nnfoctbdj  47435  iundjiun  47439  meadjiunlem  47444  voliunsge0lem  47451  meaiuninclem  47459  meaiininc2  47467  carageniuncllem1  47500  carageniuncllem2  47501  caratheodorylem1  47505  caratheodorylem2  47506  isomenndlem  47509  ovnsupge0  47536  ovnlerp  47541  ovncvrrp  47543  ovnsubaddlem1  47549  hoidmvval0  47566  hoidmv1lelem3  47572  hoidmv1le  47573  hoidmvlelem1  47574  hoidmvlelem2  47575  hoidmvlelem3  47576  ovnhoilem2  47581  opnvonmbllem2  47612  ovnovollem3  47637  vonioo  47661  vonicc  47664  pimiooltgt  47689  smfaddlem1  47742  smflimlem6  47755  smfmullem4  47773  smfpimbor1lem1  47777  smfco  47781  smfpimcc  47787  smflimmpt  47789  smfinflem  47796  smflimsuplem7  47805  smflimsuplem8  47806  smflimsupmpt  47808  smfliminfmpt  47811  cfsetsnfsetf1  48098  nnmul2b  48370  2tceilhalfelfzo1  48375  elsetpreimafveqfv  48443  iccpartiltu  48473  sprsymrelfvlem  48541  reuopreuprim  48577  nprmmul2  48579  goldbachth  48601  fmtnofac1  48624  prmdvdsfmtnof1lem1  48638  lighneal  48665  grimuhgr  48954  uhgrimedgi  48957  uhgrimisgrgriclem  48997  clnbgrgrim  49001  grimedg  49002  usgrgrtrirex  49017  isubgr3stgrlem3  49035  isubgr3stgrlem6  49038  uspgrlimlem2  49056  grlimgrtri  49070  grlicsym  49080  clnbgr3stgrgrlic  49087  gpgusgralem  49123  gpgedgvtx1  49129  gpgvtxedg0  49130  gpgvtxedg1  49131  uspgropssxp  49211  rngccatidALTV  49338  ringccatidALTV  49372  lcosslsp  49519  fllog2  49649  dignn0flhalf  49699  fv1arycl  49718  1arymaptf1  49723  fv2arycl  49729  2arymaptf1  49734  itschlc0yqe  49841  itsclc0xyqsol  49849  seposep  50003  iscnrm3lem6  50015  iunord  50753