Theorem 3exp 1256

Description: Exportation inference. (Contributed by NM, 30-May-1994.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3exp	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem 3exp

Step	Hyp	Ref	Expression
1		pm3.2an3 1233	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜑 ∧ 𝜓 ∧ 𝜒))))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl8 74	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3expa  1257  3expb  1258  3expia  1259  3expib  1260  3com23  1263  3imp3i2an  1270  3an1rs  1271  3exp1  1275  3expd  1276  exp5o  1278  ad4ant123  1286  ad4ant124  1287  ad4ant134  1288  ad4ant234  1291  ad5ant245  1299  ad5ant234  1300  ad5ant235  1301  ad5ant123  1302  ad5ant124  1303  ad5ant125  1304  ad5ant134  1305  ad5ant135  1306  ad5ant145  1307  syl3an2  1352  syl3an3  1353  syl2an23an  1379  3ecase  1429  rexlimdv3a  3015  rabssdv  3645  reupick2  3872  otiunsndisj  4905  wefrc  5032  predpo  5615  tz7.7  5666  unizlim  5761  fveqdmss  6262  f1oiso2  6502  ssorduni  6877  suceloni  6905  tfisi  6950  poxp  7176  smo11  7348  tfrlem5  7363  odi  7546  omass  7547  nndi  7590  nnmass  7591  undifixp  7830  findcard  8084  ac6sfi  8089  domunfican  8118  mapfien2  8197  fisup2g  8257  fiinf2g  8289  indcardi  8747  acndom  8757  ackbij1lem16  8940  infpssrlem4  9011  fin23lem11  9022  isfin2-2  9024  fin23lem34  9051  fin1a2lem10  9114  hsmexlem2  9132  axcc3  9143  domtriomlem  9147  axdc3lem2  9156  axdc3lem4  9158  axcclem  9162  ttukeyg  9222  axdclem2  9225  axacndlem4  9311  axacndlem5  9312  axacnd  9313  tskr1om2  9469  tskwe2  9474  tskord  9481  tskcard  9482  tskuni  9484  tskwun  9485  gruiin  9511  grudomon  9518  gruina  9519  mulcanpi  9601  adderpq  9657  mulerpq  9658  dedekindle  10080  divgt0  10770  divge0  10771  uzind  11345  uzind2  11346  iccsplit  12176  ssnn0fi  12646  sqlecan  12833  modexp  12861  facavg  12950  fundmge2nop0  13129  2cshwcshw  13422  relexpcnv  13623  relexpreld  13628  relexpaddnn  13639  relexpaddg  13641  prodfn0  14465  prodfrec  14466  ntrivcvgfvn0  14470  fprodabs  14543  fprodle  14566  bpolycl  14622  bpolydif  14625  fprodefsum  14664  dvdsaddre2b  14867  dvdsnprmd  15241  prmndvdsfaclt  15273  ncoprmlnprm  15274  pceu  15389  mreexexd  16131  mreexexdOLD  16132  initoeu1  16484  termoeu1  16491  isglbd  16940  mulgaddcom  17387  pmtrfrn  17701  psgnunilem4  17740  mulgass2  18424  islss4  18783  lspsneu  18944  lspfixed  18949  lspexch  18950  lsmcv  18962  lspsolvlem  18963  xrsdsreclblem  19611  isphld  19818  mdetralt  20233  mdetunilem9  20245  fiinopn  20531  neips  20727  tpnei  20735  neindisj2  20737  opnneiid  20740  hausnei2  20967  cmpsublem  21012  cmpsub  21013  cmpcld  21015  comppfsc  21145  filufint  21534  cfinufil  21542  rnelfm  21567  alexsubALTlem1  21661  alexsubALTlem4  21664  alexsubALT  21665  tsmsxp  21768  neibl  22116  tngngp3  22270  tgqioo  22411  ovolunlem2  23073  iunmbl2  23132  itg1le  23286  vieta1  23871  aannenlem2  23888  aalioulem3  23893  aalioulem4  23894  aaliou2  23899  wilthlem3  24596  bcmono  24802  gausslemma2dlem1a  24890  axcontlem7  25650  usgrafisinds  25942  cusgrasize2inds  26005  1pthoncl  26122  wlkdvspth  26138  nvnencycllem  26171  wwlknred  26251  wwlknextbi  26253  clwlkfclwwlk  26371  cusgraiffrusgra  26467  n4cyclfrgra  26545  vdgfrgragt2  26554  usgn0fidegnn0  26556  frgraregord013  26645  chintcli  27574  spansnss  27814  elspansn4  27816  chscllem4  27883  hoadddir  28047  adjmul  28335  kbass6  28364  spansncv2  28536  sumdmdii  28658  nexple  29399  bnj1417  30363  mclsind  30721  iprodefisumlem  30879  poseq  30994  btwndiff  31304  elicc3  31481  finminlem  31482  sdclem2  32708  clmgmOLD  32820  grpomndo  32844  zerdivemp1x  32916  lsmsat  33313  lsmcv2  33334  lcvat  33335  lsatcveq0  33337  lcvexchlem4  33342  lcvexchlem5  33343  islshpcv  33358  l1cvpat  33359  lshpkrlem6  33420  omlfh3N  33564  cvlsupr4  33650  cvlsupr5  33651  cvlsupr6  33652  2llnneN  33713  hlrelat3  33716  cvrval3  33717  cvrval4N  33718  cvrexchlem  33723  2atlt  33743  cvrat4  33747  atbtwnexOLDN  33751  atbtwnex  33752  athgt  33760  3dim1  33771  3dim2  33772  3dim3  33773  1cvratex  33777  llnle  33822  atcvrlln2  33823  atcvrlln  33824  2llnmat  33828  lplnle  33844  lplnnle2at  33845  lplnnlelln  33847  llncvrlpln2  33861  2llnjN  33871  lvoli2  33885  lvolnlelln  33888  lvolnlelpln  33889  4atlem10  33910  4atlem11  33913  4atlem12  33916  lplncvrlvol2  33919  2lplnj  33924  lneq2at  34082  lnatexN  34083  lnjatN  34084  lncvrat  34086  2lnat  34088  cdlemb  34098  paddasslem14  34137  llnexchb2  34173  dalawlem10  34184  dalawlem13  34187  dalawlem14  34188  dalaw  34190  pclclN  34195  pclfinN  34204  osumcllem11N  34270  lhp2lt  34305  lhpexle3lem  34315  4atexlem7  34379  ldilcnv  34419  ldilco  34420  ltrncnv  34450  trlval2  34468  cdleme24  34658  cdleme26ee  34666  cdleme28  34679  cdleme32le  34753  cdleme50trn2  34857  cdleme50ltrn  34863  cdleme  34866  cdlemf1  34867  cdlemf  34869  cdlemg1cex  34894  cdlemg2ce  34898  cdlemg18b  34985  ltrnco  35025  tendocan  35130  cdlemk28-3  35214  cdlemk11t  35252  dia2dimlem6  35376  dia2dimlem12  35382  dihlsscpre  35541  dihord4  35565  dihord5b  35566  dihmeetlem3N  35612  dihmeetlem20N  35633  dvh4dimlem  35750  lclkrlem2y  35838  mapdpglem24  36011  mapdpglem32  36012  mapdpg  36013  baerlem3lem2  36017  baerlem5alem2  36018  baerlem5blem2  36019  mapdh9a  36097  mapdh9aOLDN  36098  hdmap14lem6  36183  hdmapglem7  36239  mzpexpmpt  36326  pellexlem5  36415  pellex  36417  pell14qrexpclnn0  36448  pellfundex  36468  monotuz  36524  monotoddzzfi  36525  expmordi  36530  rmxypos  36532  jm2.17a  36545  jm2.17b  36546  rmygeid  36549  jm2.19lem3  36576  jm2.15nn0  36588  jm2.16nn0  36589  aomclem2  36643  aomclem6  36647  dfac11  36650  hbtlem5  36717  cnsrexpcl  36754  relexpxpnnidm  37014  relexpiidm  37015  relexpss1d  37016  iunrelexpmin1  37019  relexpmulnn  37020  iunrelexpmin2  37023  relexp01min  37024  relexp0a  37027  relexpxpmin  37028  relexpaddss  37029  trclimalb2  37037  3impexpbicomi  37707  ee333  37734  eel12131  37959  eel2122old  37964  e333  37981  ordelordALTVD  38125  refsumcn  38212  uzwo4  38246  ssinc  38292  ssdec  38293  iunincfi  38300  eliuniin  38307  restuni3  38333  eliuniin2  38335  suprnmpt  38350  wessf1ornlem  38366  disjf1o  38373  fompt  38374  disjinfi  38375  ssnnf1octb  38377  mapsnd  38383  choicefi  38387  mapssbi  38400  unirnmapsn  38401  ssmapsn  38403  iunmapsn  38404  fperiodmullem  38458  upbdrech  38460  ssfiunibd  38464  supxrgere  38490  iuneqfzuzlem  38491  supxrgelem  38494  supxrge  38495  suplesup  38496  infrpge  38508  infleinf  38529  suplesup2  38533  iccshift  38591  iooshift  38595  fmul01  38647  fmuldfeq  38650  fmul01lt1  38653  mullimc  38683  islptre  38686  mullimcf  38690  limcperiod  38695  islpcn  38706  limsupre  38708  limcleqr  38711  neglimc  38714  addlimc  38715  0ellimcdiv  38716  limclner  38718  fnlimfvre  38741  coskpi2  38749  cosknegpi  38752  cncfshift  38759  cncfperiod  38764  icccncfext  38773  dvnmptdivc  38828  dvnmptconst  38831  dvnmul  38833  dvmptfprodlem  38834  dvmptfprod  38835  dvnprodlem1  38836  dvnprodlem2  38837  iblspltprt  38865  itgspltprt  38871  itgperiod  38873  ismbl3  38879  stoweidlem3  38896  stoweidlem31  38924  stoweidlem59  38952  stirlinglem13  38979  fourierdlem41  39041  fourierdlem42  39042  fourierdlem48  39047  fourierdlem51  39050  fourierdlem53  39052  fourierdlem70  39069  fourierdlem71  39070  fourierdlem73  39072  fourierdlem80  39079  fourierdlem81  39080  fourierdlem89  39088  fourierdlem91  39090  fourierdlem93  39092  fourierdlem97  39096  elaa2  39127  qndenserrnopnlem  39193  salexct  39228  subsaliuncl  39252  subsalsal  39253  sge0tsms  39273  sge0f1o  39275  sge0fsum  39280  sge0supre  39282  sge0sup  39284  sge0rnbnd  39286  sge0gerp  39288  sge0pnffigt  39289  sge0lefi  39291  sge0ltfirp  39293  sge0resrn  39297  sge0resplit  39299  sge0split  39302  sge0iunmptlemfi  39306  sge0iunmptlemre  39308  sge0iunmpt  39311  sge0rpcpnf  39314  sge0isum  39320  sge0xp  39322  sge0xaddlem2  39327  sge0uzfsumgt  39337  sge0seq  39339  sge0reuz  39340  nnfoctbdjlem  39348  nnfoctbdj  39349  iundjiun  39353  meadjiunlem  39358  voliunsge0lem  39365  meaiuninclem  39373  meaiininc2  39378  carageniuncllem1  39411  carageniuncllem2  39412  caratheodorylem1  39416  caratheodorylem2  39417  isomenndlem  39420  ovnsupge0  39447  ovnlerp  39452  ovncvrrp  39454  ovnsubaddlem1  39460  hoidmvval0  39477  hoidmv1lelem3  39483  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  ovnhoilem2  39492  opnvonmbllem2  39523  ovolval5lem3  39544  ovnovollem3  39548  vonioo  39573  vonicc  39576  pimiooltgt  39598  sssmf  39625  smfaddlem1  39649  smflimlem6  39662  smfmullem4  39679  smfpimbor1lem1  39683  smfco  39687  iccpartiltu  39960  goldbachth  39997  fmtnofac1  40020  prmdvdsfmtnof1lem1  40034  pwdif  40039  lighneal  40066  uhgrauhgrbi  40377  ausgrumgri  40397  ausgrusgri  40398  usgrausgrb  40399  usgredg2vtxeuALT  40449  ushgredgedga  40456  ushgredgedgaloop  40458  nbuhgr2vtx1edgb  40574  cusgrsize2inds  40669  upgrewlkle2  40808  1wlkl1loop  40842  red1wlk  40881  pthdivtx  40935  pthdadjvtx  40936  upgr2pthnlp  40938  upgrspths1wlk  40944  clwlkl1loop  40989  cyclnsPth  41006  wwlksnred  41098  wwlksnextbi  41100  elwwlks2ons3  41159  umgrwwlks2on  41161  clwwnisshclwwsn  41237  clwlksfclwwlk  41269  1pthon2v-av  41320  uhgr3cyclex  41349  n4cyclfrgr  41461  fusgr2wsp2nb  41498  av-numclwwlkffin0  41513  av-frgrareggt1  41547  av-frgrareg  41548  av-frgraregord013  41549  rngccatidALTV  41781  ringccatidALTV  41844  nzerooringczr  41864  lcosslsp  42021  fllog2  42160  dignn0flhalf  42210  iunord  42220  setrec2fun  42238