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

Theorem 3exp 1255
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 1232 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜑𝜓𝜒))))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl8 73 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  3expa  1256  3expb  1257  3expia  1258  3expib  1259  3com23  1262  3imp3i2an  1269  3an1rs  1270  3exp1  1274  3expd  1275  exp5o  1277  ad4ant123  1285  ad4ant124  1286  ad4ant134  1287  ad4ant234  1290  ad5ant245  1298  ad5ant234  1299  ad5ant235  1300  ad5ant123  1301  ad5ant124  1302  ad5ant125  1303  ad5ant134  1304  ad5ant135  1305  ad5ant145  1306  syl3an2  1351  syl3an3  1352  syl2an23an  1378  3ecase  1428  rexlimdv3a  3014  rabssdv  3644  reupick2  3871  otiunsndisj  4896  wefrc  5022  predpo  5601  tz7.7  5652  unizlim  5747  fveqdmss  6247  f1oiso2  6480  ssorduni  6854  suceloni  6882  tfisi  6927  poxp  7153  smo11  7325  tfrlem5  7340  odi  7523  omass  7524  nndi  7567  nnmass  7568  undifixp  7807  findcard  8061  ac6sfi  8066  domunfican  8095  mapfien2  8174  fisup2g  8234  fiinf2g  8266  indcardi  8724  acndom  8734  ackbij1lem16  8917  infpssrlem4  8988  fin23lem11  8999  isfin2-2  9001  fin23lem34  9028  fin1a2lem10  9091  hsmexlem2  9109  axcc3  9120  domtriomlem  9124  axdc3lem2  9133  axdc3lem4  9135  axcclem  9139  ttukeyg  9199  axdclem2  9202  axacndlem4  9288  axacndlem5  9289  axacnd  9290  tskr1om2  9446  tskwe2  9451  tskord  9458  tskcard  9459  tskuni  9461  tskwun  9462  gruiin  9488  grudomon  9495  gruina  9496  mulcanpi  9578  adderpq  9634  mulerpq  9635  dedekindle  10052  divgt0  10740  divge0  10741  uzind  11301  uzind2  11302  iccsplit  12132  ssnn0fi  12601  sqlecan  12788  modexp  12816  facavg  12905  2cshwcshw  13368  relexpcnv  13569  relexpreld  13574  relexpaddnn  13585  relexpaddg  13587  prodfn0  14411  prodfrec  14412  ntrivcvgfvn0  14416  fprodabs  14489  fprodle  14512  bpolycl  14568  bpolydif  14571  fprodefsum  14610  dvdsaddre2b  14813  dvdsnprmd  15187  prmndvdsfaclt  15219  ncoprmlnprm  15220  pceu  15335  mreexexd  16077  mreexexdOLD  16078  initoeu1  16430  termoeu1  16437  isglbd  16886  mulgaddcom  17333  pmtrfrn  17647  psgnunilem4  17686  mulgass2  18370  islss4  18729  lspsneu  18890  lspfixed  18895  lspexch  18896  lsmcv  18908  lspsolvlem  18909  xrsdsreclblem  19557  isphld  19763  mdetralt  20175  mdetunilem9  20187  fiinopn  20473  neips  20669  tpnei  20677  neindisj2  20679  opnneiid  20682  hausnei2  20909  cmpsublem  20954  cmpsub  20955  cmpcld  20957  comppfsc  21087  filufint  21476  cfinufil  21484  rnelfm  21509  alexsubALTlem1  21603  alexsubALTlem4  21606  alexsubALT  21607  tsmsxp  21710  neibl  22057  tgqioo  22343  ovolunlem2  22990  iunmbl2  23049  itg1le  23203  vieta1  23788  aannenlem2  23805  aalioulem3  23810  aalioulem4  23811  aaliou2  23816  wilthlem3  24513  bcmono  24719  gausslemma2dlem1a  24807  axcontlem7  25568  usgrafisinds  25708  cusgrasize2inds  25771  1pthoncl  25888  wlkdvspth  25904  nvnencycllem  25937  wwlknred  26017  wwlknextbi  26019  clwlkfclwwlk  26137  cusgraiffrusgra  26233  n4cyclfrgra  26311  vdgfrgragt2  26320  usgn0fidegnn0  26322  frgraregord013  26411  chintcli  27380  spansnss  27620  elspansn4  27622  chscllem4  27689  hoadddir  27853  adjmul  28141  kbass6  28170  spansncv2  28342  sumdmdii  28464  nexple  29205  bnj1417  30169  mclsind  30527  iprodefisumlem  30685  poseq  30800  btwndiff  31110  elicc3  31287  finminlem  31288  sdclem2  32504  clmgmOLD  32616  grpomndo  32640  zerdivemp1x  32712  lsmsat  33109  lsmcv2  33130  lcvat  33131  lsatcveq0  33133  lcvexchlem4  33138  lcvexchlem5  33139  islshpcv  33154  l1cvpat  33155  lshpkrlem6  33216  omlfh3N  33360  cvlsupr4  33446  cvlsupr5  33447  cvlsupr6  33448  2llnneN  33509  hlrelat3  33512  cvrval3  33513  cvrval4N  33514  cvrexchlem  33519  2atlt  33539  cvrat4  33543  atbtwnexOLDN  33547  atbtwnex  33548  athgt  33556  3dim1  33567  3dim2  33568  3dim3  33569  1cvratex  33573  llnle  33618  atcvrlln2  33619  atcvrlln  33620  2llnmat  33624  lplnle  33640  lplnnle2at  33641  lplnnlelln  33643  llncvrlpln2  33657  2llnjN  33667  lvoli2  33681  lvolnlelln  33684  lvolnlelpln  33685  4atlem10  33706  4atlem11  33709  4atlem12  33712  lplncvrlvol2  33715  2lplnj  33720  lneq2at  33878  lnatexN  33879  lnjatN  33880  lncvrat  33882  2lnat  33884  cdlemb  33894  paddasslem14  33933  llnexchb2  33969  dalawlem10  33980  dalawlem13  33983  dalawlem14  33984  dalaw  33986  pclclN  33991  pclfinN  34000  osumcllem11N  34066  lhp2lt  34101  lhpexle3lem  34111  4atexlem7  34175  ldilcnv  34215  ldilco  34216  ltrncnv  34246  trlval2  34264  cdleme24  34454  cdleme26ee  34462  cdleme28  34475  cdleme32le  34549  cdleme50trn2  34653  cdleme50ltrn  34659  cdleme  34662  cdlemf1  34663  cdlemf  34665  cdlemg1cex  34690  cdlemg2ce  34694  cdlemg18b  34781  ltrnco  34821  tendocan  34926  cdlemk28-3  35010  cdlemk11t  35048  dia2dimlem6  35172  dia2dimlem12  35178  dihlsscpre  35337  dihord4  35361  dihord5b  35362  dihmeetlem3N  35408  dihmeetlem20N  35429  dvh4dimlem  35546  lclkrlem2y  35634  mapdpglem24  35807  mapdpglem32  35808  mapdpg  35809  baerlem3lem2  35813  baerlem5alem2  35814  baerlem5blem2  35815  mapdh9a  35893  mapdh9aOLDN  35894  hdmap14lem6  35979  hdmapglem7  36035  mzpexpmpt  36122  pellexlem5  36211  pellex  36213  pell14qrexpclnn0  36244  pellfundex  36264  monotuz  36320  monotoddzzfi  36321  expmordi  36326  rmxypos  36328  jm2.17a  36341  jm2.17b  36342  rmygeid  36345  jm2.19lem3  36372  jm2.15nn0  36384  jm2.16nn0  36385  aomclem2  36439  aomclem6  36443  dfac11  36446  hbtlem5  36513  cnsrexpcl  36550  relexpxpnnidm  36810  relexpiidm  36811  relexpss1d  36812  iunrelexpmin1  36815  relexpmulnn  36816  iunrelexpmin2  36819  relexp01min  36820  relexp0a  36823  relexpxpmin  36824  relexpaddss  36825  trclimalb2  36833  3impexpbicomi  37503  ee333  37530  eel12131  37755  eel2122old  37760  e333  37777  ordelordALTVD  37921  refsumcn  38008  uzwo4  38042  ssinc  38088  ssdec  38089  iunincfi  38096  eliuniin  38103  restuni3  38129  eliuniin2  38131  suprnmpt  38146  wessf1ornlem  38162  disjf1o  38169  fompt  38170  disjinfi  38171  ssnnf1octb  38173  mapsnd  38179  choicefi  38183  mapssbi  38196  unirnmapsn  38197  ssmapsn  38199  iunmapsn  38200  fperiodmullem  38254  upbdrech  38256  ssfiunibd  38260  supxrgere  38287  iuneqfzuzlem  38288  supxrgelem  38291  supxrge  38292  suplesup  38293  infrpge  38305  infleinf  38326  suplesup2  38330  iccshift  38388  iooshift  38392  fmul01  38444  fmuldfeq  38447  fmul01lt1  38450  mullimc  38480  islptre  38483  mullimcf  38487  limcperiod  38492  islpcn  38503  limsupre  38505  limcleqr  38508  neglimc  38511  addlimc  38512  0ellimcdiv  38513  limclner  38515  fnlimfvre  38538  coskpi2  38546  cosknegpi  38549  cncfshift  38556  cncfperiod  38561  icccncfext  38570  dvnmptdivc  38625  dvnmptconst  38628  dvnmul  38630  dvmptfprodlem  38631  dvmptfprod  38632  dvnprodlem1  38633  dvnprodlem2  38634  iblspltprt  38662  itgspltprt  38668  itgperiod  38670  ismbl3  38676  stoweidlem3  38693  stoweidlem31  38721  stoweidlem59  38749  stirlinglem13  38776  fourierdlem41  38838  fourierdlem42  38839  fourierdlem48  38844  fourierdlem51  38847  fourierdlem53  38849  fourierdlem70  38866  fourierdlem71  38867  fourierdlem73  38869  fourierdlem80  38876  fourierdlem81  38877  fourierdlem89  38885  fourierdlem91  38887  fourierdlem93  38889  fourierdlem97  38893  elaa2  38924  qndenserrnopnlem  38990  salexct  39025  subsaliuncl  39049  subsalsal  39050  sge0tsms  39070  sge0f1o  39072  sge0fsum  39077  sge0supre  39079  sge0sup  39081  sge0rnbnd  39083  sge0gerp  39085  sge0pnffigt  39086  sge0lefi  39088  sge0ltfirp  39090  sge0resrn  39094  sge0resplit  39096  sge0split  39099  sge0iunmptlemfi  39103  sge0iunmptlemre  39105  sge0iunmpt  39108  sge0rpcpnf  39111  sge0isum  39117  sge0xp  39119  sge0xaddlem2  39124  sge0uzfsumgt  39134  sge0seq  39136  sge0reuz  39137  nnfoctbdjlem  39145  nnfoctbdj  39146  iundjiun  39150  meadjiunlem  39155  voliunsge0lem  39162  meaiuninclem  39170  meaiininc2  39175  carageniuncllem1  39208  carageniuncllem2  39209  caratheodorylem1  39213  caratheodorylem2  39214  isomenndlem  39217  ovnsupge0  39244  ovnlerp  39249  ovncvrrp  39251  ovnsubaddlem1  39257  hoidmvval0  39274  hoidmv1lelem3  39280  hoidmv1le  39281  hoidmvlelem1  39282  hoidmvlelem2  39283  hoidmvlelem3  39284  ovnhoilem2  39289  opnvonmbllem2  39320  ovolval5lem3  39341  ovnovollem3  39345  vonioo  39370  vonicc  39373  pimiooltgt  39395  sssmf  39422  smfaddlem1  39446  smflimlem6  39459  smfmullem4  39476  smfpimbor1lem1  39480  smfco  39484  iccpartiltu  39758  goldbachth  39795  fmtnofac1  39818  prmdvdsfmtnof1lem1  39832  pwdif  39837  lighneal  39864  fundmge2nop0  40145  uhgrauhgrbi  40289  ausgrumgri  40392  ausgrusgri  40393  usgrausgrb  40394  usgredg2vtxeuALT  40444  ushgredgedga  40451  ushgredgedgaloop  40453  nbuhgr2vtx1edgb  40569  cusgrsize2inds  40664  upgrewlkle2  40803  1wlkl1loop  40837  red1wlk  40876  pthdivtx  40930  pthdadjvtx  40931  upgr2pthnlp  40933  upgrspths1wlk  40939  clwlkl1loop  40984  cyclnsPth  41001  wwlksnred  41093  wwlksnextbi  41095  elwwlks2ons3  41154  umgrwwlks2on  41156  clwwnisshclwwsn  41232  clwlksfclwwlk  41264  1pthon2v-av  41315  uhgr3cyclex  41344  n4cyclfrgr  41456  fusgr2wsp2nb  41493  av-numclwwlkffin0  41508  av-frgrareggt1  41542  av-frgrareg  41543  av-frgraregord013  41544  rngccatidALTV  41776  ringccatidALTV  41839  nzerooringczr  41859  lcosslsp  42016  fllog2  42155  dignn0flhalf  42205
  Copyright terms: Public domain W3C validator