MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3exp Structured version   Visualization version   GIF version

Theorem 3exp 1262
Description: Exportation inference. (Contributed by NM, 30-May-1994.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3exp (𝜑 → (𝜓 → (𝜒𝜃)))

Proof of Theorem 3exp
StepHypRef Expression
1 pm3.2an3 1238 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜑𝜓𝜒))))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl8 76 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  3expa  1263  3expb  1264  3expia  1265  3expib  1266  3com23  1269  3imp3i2an  1276  3an1rs  1277  3exp1  1281  3expd  1282  exp5o  1284  ad4ant123  1292  ad4ant124  1293  ad4ant134  1294  ad4ant234  1297  ad5ant245  1305  ad5ant234  1306  ad5ant235  1307  ad5ant123  1308  ad5ant124  1309  ad5ant125  1310  ad5ant134  1311  ad5ant135  1312  ad5ant145  1313  syl3an2  1358  syl3an3  1359  syl2an23an  1385  3ecase  1435  rexlimdv3a  3029  rabssdv  3674  reupick2  3905  disjiund  4634  otiunsndisj  4970  wefrc  5098  predpo  5686  tz7.7  5737  unizlim  5832  fveqdmss  6340  f1oiso2  6587  ssorduni  6970  suceloni  6998  tfisi  7043  poxp  7274  smo11  7446  tfrlem5  7461  odi  7644  omass  7645  nndi  7688  nnmass  7689  undifixp  7929  findcard  8184  ac6sfi  8189  domunfican  8218  mapfien2  8299  fisup2g  8359  fiinf2g  8391  indcardi  8849  acndom  8859  ackbij1lem16  9042  infpssrlem4  9113  fin23lem11  9124  isfin2-2  9126  fin23lem34  9153  fin1a2lem10  9216  hsmexlem2  9234  axcc3  9245  domtriomlem  9249  axdc3lem2  9258  axdc3lem4  9260  axcclem  9264  ttukeyg  9324  axdclem2  9327  axacndlem4  9417  axacndlem5  9418  axacnd  9419  tskr1om2  9575  tskwe2  9580  tskord  9587  tskcard  9588  tskuni  9590  tskwun  9591  gruiin  9617  grudomon  9624  gruina  9625  mulcanpi  9707  adderpq  9763  mulerpq  9764  dedekindle  10186  divgt0  10876  divge0  10877  uzind  11454  uzind2  11455  iccsplit  12290  ssnn0fi  12767  sqlecan  12954  modexp  12982  facavg  13071  2cshwcshw  13552  relexpcnv  13756  relexpreld  13761  relexpaddnn  13772  relexpaddg  13774  prodfn0  14607  prodfrec  14608  ntrivcvgfvn0  14612  fprodabs  14685  fprodle  14708  bpolycl  14764  bpolydif  14767  fprodefsum  14806  dvdsaddre2b  15010  dvdsnprmd  15384  prmndvdsfaclt  15416  ncoprmlnprm  15417  pceu  15532  setsstruct2  15877  setsstruct  15879  mreexexd  16289  mreexexdOLD  16290  initoeu1  16642  termoeu1  16649  isglbd  17098  mulgaddcom  17545  pmtrfrn  17859  psgnunilem4  17898  mulgass2  18582  islss4  18943  lspsneu  19104  lspfixed  19109  lspexch  19110  lsmcv  19122  lspsolvlem  19123  xrsdsreclblem  19773  isphld  19980  mdetralt  20395  mdetunilem9  20407  fiinopn  20687  neips  20898  tpnei  20906  neindisj2  20908  opnneiid  20911  hausnei2  21138  cmpsublem  21183  cmpsub  21184  cmpcld  21186  comppfsc  21316  filufint  21705  cfinufil  21713  rnelfm  21738  alexsubALTlem1  21832  alexsubALTlem4  21835  alexsubALT  21836  tsmsxp  21939  neibl  22287  tngngp3  22441  tgqioo  22584  ovolunlem2  23247  iunmbl2  23306  itg1le  23461  vieta1  24048  aannenlem2  24065  aalioulem3  24070  aalioulem4  24071  aaliou2  24076  wilthlem3  24777  bcmono  24983  gausslemma2dlem1a  25071  axcontlem7  25831  edglnl  26019  numedglnl  26020  ausgrumgri  26043  ausgrusgri  26044  usgrausgrb  26045  usgredg2vtxeuALT  26095  ushgredgedg  26102  ushgredgedgloop  26104  nbuhgr2vtx1edgb  26229  cusgrsize2inds  26330  upgrewlkle2  26483  wlkl1loop  26515  redwlk  26550  pthdivtx  26606  pthdadjvtx  26607  upgr2pthnlp  26609  upgrspthswlk  26615  clwlkl1loop  26659  wwlksnred  26768  wwlksnextbi  26770  elwwlks2ons3  26829  umgrwwlks2on  26831  clwwnisshclwwsn  26910  clwlksfclwwlk  26942  1pthon2v  26993  uhgr3cyclex  27022  n4cyclfrgr  27135  frgrwopreg  27159  numclwwlkffin0  27187  frgrreggt1  27221  frgrreg  27222  frgrregord013  27223  chintcli  28160  spansnss  28400  elspansn4  28402  chscllem4  28469  hoadddir  28633  adjmul  28921  kbass6  28950  spansncv2  29122  sumdmdii  29244  nexple  30045  bnj1417  31083  mclsind  31441  iprodefisumlem  31601  poseq  31724  btwndiff  32109  elicc3  32286  finminlem  32287  sdclem2  33509  clmgmOLD  33621  grpomndo  33645  zerdivemp1x  33717  lsmsat  34114  lsmcv2  34135  lcvat  34136  lsatcveq0  34138  lcvexchlem4  34143  lcvexchlem5  34144  islshpcv  34159  l1cvpat  34160  lshpkrlem6  34221  omlfh3N  34365  cvlsupr4  34451  cvlsupr5  34452  cvlsupr6  34453  2llnneN  34514  hlrelat3  34517  cvrval3  34518  cvrval4N  34519  cvrexchlem  34524  2atlt  34544  cvrat4  34548  atbtwnexOLDN  34552  atbtwnex  34553  athgt  34561  3dim1  34572  3dim2  34573  3dim3  34574  1cvratex  34578  llnle  34623  atcvrlln2  34624  atcvrlln  34625  2llnmat  34629  lplnle  34645  lplnnle2at  34646  lplnnlelln  34648  llncvrlpln2  34662  2llnjN  34672  lvoli2  34686  lvolnlelln  34689  lvolnlelpln  34690  4atlem10  34711  4atlem11  34714  4atlem12  34717  lplncvrlvol2  34720  2lplnj  34725  lneq2at  34883  lnatexN  34884  lnjatN  34885  lncvrat  34887  2lnat  34889  cdlemb  34899  paddasslem14  34938  llnexchb2  34974  dalawlem10  34985  dalawlem13  34988  dalawlem14  34989  dalaw  34991  pclclN  34996  pclfinN  35005  osumcllem11N  35071  lhp2lt  35106  lhpexle3lem  35116  4atexlem7  35180  ldilcnv  35220  ldilco  35221  ltrncnv  35251  trlval2  35269  cdleme24  35459  cdleme26ee  35467  cdleme28  35480  cdleme32le  35554  cdleme50trn2  35658  cdleme50ltrn  35664  cdleme  35667  cdlemf1  35668  cdlemf  35670  cdlemg1cex  35695  cdlemg2ce  35699  cdlemg18b  35786  ltrnco  35826  tendocan  35931  cdlemk28-3  36015  cdlemk11t  36053  dia2dimlem6  36177  dia2dimlem12  36183  dihlsscpre  36342  dihord4  36366  dihord5b  36367  dihmeetlem3N  36413  dihmeetlem20N  36434  dvh4dimlem  36551  lclkrlem2y  36639  mapdpglem24  36812  mapdpglem32  36813  mapdpg  36814  baerlem3lem2  36818  baerlem5alem2  36819  baerlem5blem2  36820  mapdh9a  36898  mapdh9aOLDN  36899  hdmap14lem6  36984  hdmapglem7  37040  mzpexpmpt  37127  pellexlem5  37216  pellex  37218  pell14qrexpclnn0  37249  pellfundex  37269  monotuz  37325  monotoddzzfi  37326  expmordi  37331  rmxypos  37333  jm2.17a  37346  jm2.17b  37347  rmygeid  37350  jm2.19lem3  37377  jm2.15nn0  37389  jm2.16nn0  37390  aomclem2  37444  aomclem6  37448  dfac11  37451  hbtlem5  37517  cnsrexpcl  37554  relexpxpnnidm  37814  relexpiidm  37815  relexpss1d  37816  iunrelexpmin1  37819  relexpmulnn  37820  iunrelexpmin2  37823  relexp01min  37824  relexp0a  37827  relexpxpmin  37828  relexpaddss  37829  trclimalb2  37837  3impexpbicomi  38506  ee333  38533  eel12131  38758  eel2122old  38763  e333  38780  ordelordALTVD  38923  refsumcn  39009  uzwo4  39041  ssinc  39084  ssdec  39085  iunincfi  39092  restuni3  39121  eliuniin2  39123  rabssd  39152  suprnmpt  39171  wessf1ornlem  39187  disjf1o  39194  fompt  39195  disjinfi  39196  ssnnf1octb  39198  mapsnd  39204  choicefi  39208  mapssbi  39221  unirnmapsn  39222  ssmapsn  39224  iunmapsn  39225  funimassd  39247  rnmptlb  39269  rnmptbddlem  39271  fvelimad  39274  infnsuprnmpt  39281  fperiodmullem  39330  upbdrech  39332  ssfiunibd  39336  supxrgere  39362  iuneqfzuzlem  39363  supxrgelem  39366  supxrge  39367  suplesup  39368  infrpge  39380  infleinf  39401  suplesup2  39405  supxrunb3  39436  infleinf2  39454  rexabslelem  39458  infrnmptle  39463  infxrunb3rnmpt  39468  iccshift  39547  iooshift  39551  fmul01  39612  fmuldfeq  39615  fmul01lt1  39618  mullimc  39648  islptre  39651  mullimcf  39655  limcperiod  39660  islpcn  39671  limsupre  39673  limcleqr  39676  neglimc  39679  addlimc  39680  0ellimcdiv  39681  limclner  39683  fnlimfvre  39706  limsuppnflem  39742  limsupmnfuzlem  39758  limsupre3lem  39764  limsupre3uzlem  39767  climuzlem  39775  limsupgtlem  39803  coskpi2  39840  cosknegpi  39843  cncfshift  39850  cncfperiod  39855  icccncfext  39863  dvnmptdivc  39916  dvnmptconst  39919  dvnmul  39921  dvmptfprodlem  39922  dvmptfprod  39923  dvnprodlem1  39924  dvnprodlem2  39925  iblspltprt  39952  itgspltprt  39958  itgperiod  39960  ismbl3  39966  stoweidlem3  39983  stoweidlem31  40011  stoweidlem59  40039  stirlinglem13  40066  fourierdlem41  40128  fourierdlem42  40129  fourierdlem48  40134  fourierdlem51  40137  fourierdlem53  40139  fourierdlem70  40156  fourierdlem71  40157  fourierdlem73  40159  fourierdlem80  40166  fourierdlem81  40167  fourierdlem89  40175  fourierdlem91  40177  fourierdlem93  40179  fourierdlem97  40183  elaa2  40214  qndenserrnopnlem  40280  salexct  40315  subsaliuncl  40339  subsalsal  40340  sge0tsms  40360  sge0f1o  40362  sge0fsum  40367  sge0supre  40369  sge0sup  40371  sge0rnbnd  40373  sge0gerp  40375  sge0pnffigt  40376  sge0lefi  40378  sge0ltfirp  40380  sge0resrn  40384  sge0resplit  40386  sge0split  40389  sge0iunmptlemfi  40393  sge0iunmptlemre  40395  sge0iunmpt  40398  sge0rpcpnf  40401  sge0isum  40407  sge0xp  40409  sge0xaddlem2  40414  sge0uzfsumgt  40424  sge0seq  40426  sge0reuz  40427  nnfoctbdjlem  40435  nnfoctbdj  40436  iundjiun  40440  meadjiunlem  40445  voliunsge0lem  40452  meaiuninclem  40460  meaiininc2  40465  carageniuncllem1  40498  carageniuncllem2  40499  caratheodorylem1  40503  caratheodorylem2  40504  isomenndlem  40507  ovnsupge0  40534  ovnlerp  40539  ovncvrrp  40541  ovnsubaddlem1  40547  hoidmvval0  40564  hoidmv1lelem3  40570  hoidmv1le  40571  hoidmvlelem1  40572  hoidmvlelem2  40573  hoidmvlelem3  40574  ovnhoilem2  40579  opnvonmbllem2  40610  ovolval5lem3  40631  ovnovollem3  40635  vonioo  40659  vonicc  40662  pimiooltgt  40684  sssmf  40710  smfaddlem1  40734  smflimlem6  40747  smfmullem4  40764  smfpimbor1lem1  40768  smfco  40772  smfpimcc  40777  smflimmpt  40779  smfinflem  40786  smflimsuplem7  40795  smflimsuplem8  40796  smflimsupmpt  40798  smfliminfmpt  40801  iccpartiltu  41122  goldbachth  41224  fmtnofac1  41247  prmdvdsfmtnof1lem1  41261  pwdif  41266  lighneal  41293  sprsymrelfvlem  41505  uspgropssxp  41517  rngccatidALTV  41754  ringccatidALTV  41817  nzerooringczr  41837  lcosslsp  41992  fllog2  42127  dignn0flhalf  42177  iunord  42187  setrec2fun  42204
  Copyright terms: Public domain W3C validator