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

Theorem 3exp 1283
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 1260 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜑𝜓𝜒))))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl8 76 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  3expa  1284  3expb  1285  3expia  1286  3expib  1287  3com23OLD  1293  3imp3i2anOLD  1300  3an1rsOLD  1301  3exp1  1305  3expd  1306  exp5o  1308  ad4ant123OLD  1320  ad4ant124OLD  1322  ad4ant134OLD  1324  ad4ant234OLD  1330  ad5ant245OLD  1345  ad5ant234OLD  1347  ad5ant235OLD  1349  ad5ant123  1350  ad5ant124  1351  ad5ant125  1352  ad5ant134  1353  ad5ant135  1354  ad5ant145  1355  syl3an2  1400  syl3an3  1401  syl2an23an  1427  3ecase  1477  rexlimdv3a  3062  rabssdv  3715  reupick2  3946  disjiund  4675  otiunsndisj  5009  wefrc  5137  predpo  5736  tz7.7  5787  unizlim  5882  fveqdmss  6394  f1oiso2  6642  ssorduni  7027  suceloni  7055  tfisi  7100  poxp  7334  smo11  7506  tfrlem5  7521  odi  7704  omass  7705  nndi  7748  nnmass  7749  undifixp  7986  findcard  8240  ac6sfi  8245  domunfican  8274  mapfien2  8355  fisup2g  8415  fiinf2g  8447  indcardi  8902  acndom  8912  ackbij1lem16  9095  infpssrlem4  9166  fin23lem11  9177  isfin2-2  9179  fin23lem34  9206  fin1a2lem10  9269  hsmexlem2  9287  axcc3  9298  domtriomlem  9302  axdc3lem2  9311  axdc3lem4  9313  axcclem  9317  ttukeyg  9377  axdclem2  9380  axacndlem4  9470  axacndlem5  9471  axacnd  9472  tskr1om2  9628  tskwe2  9633  tskord  9640  tskcard  9641  tskuni  9643  tskwun  9644  gruiin  9670  grudomon  9677  gruina  9678  mulcanpi  9760  adderpq  9816  mulerpq  9817  dedekindle  10239  divgt0  10929  divge0  10930  uzind  11507  uzind2  11508  iccsplit  12343  ssnn0fi  12824  sqlecan  13011  modexp  13039  facavg  13128  2cshwcshw  13617  relexpcnv  13819  relexpreld  13824  relexpaddnn  13835  relexpaddg  13837  prodfn0  14670  prodfrec  14671  ntrivcvgfvn0  14675  fprodabs  14748  fprodle  14771  bpolycl  14827  bpolydif  14830  fprodefsum  14869  dvdsmodexp  15035  dvdsaddre2b  15076  dvdsnprmd  15450  prmndvdsfaclt  15482  ncoprmlnprm  15483  fermltl  15536  pceu  15598  setsstruct2  15943  setsstruct  15945  mreexexd  16355  mreexexdOLD  16356  initoeu1  16708  termoeu1  16715  isglbd  17164  mulgaddcom  17611  pmtrfrn  17924  psgnunilem4  17963  mulgass2  18647  islss4  19010  lspsneu  19171  lspfixed  19176  lspexch  19177  lsmcv  19189  lspsolvlem  19190  xrsdsreclblem  19840  isphld  20047  mdetralt  20462  mdetunilem9  20474  fiinopn  20754  neips  20965  tpnei  20973  neindisj2  20975  opnneiid  20978  hausnei2  21205  cmpsublem  21250  cmpsub  21251  cmpcld  21253  comppfsc  21383  filufint  21771  cfinufil  21779  rnelfm  21804  alexsubALTlem1  21898  alexsubALTlem4  21901  alexsubALT  21902  tsmsxp  22005  neibl  22353  tngngp3  22507  tgqioo  22650  ovolunlem2  23312  iunmbl2  23371  itg1le  23525  vieta1  24112  aannenlem2  24129  aalioulem3  24134  aalioulem4  24135  aaliou2  24140  wilthlem3  24841  bcmono  25047  gausslemma2dlem1a  25135  axcontlem7  25895  edglnl  26083  numedglnl  26084  ausgrumgri  26107  ausgrusgri  26108  usgrausgrb  26109  usgredg2vtxeuALT  26159  ushgredgedg  26166  ushgredgedgloop  26168  nbuhgr2vtx1edgb  26293  cusgrsize2inds  26405  upgrewlkle2  26558  wlkl1loop  26590  redwlk  26625  pthdivtx  26681  pthdadjvtx  26682  upgr2pthnlp  26684  upgrspthswlk  26690  clwlkl1loop  26734  wwlksnred  26855  wwlksnextbi  26857  elwwlks2ons3im  26919  elwwlks2ons3OLD  26921  umgrwwlks2on  26923  clwwlknwwlksn  27000  clwwlknwwlksnOLD  27001  clwwlkinwwlk  27003  wwlksext2clwwlk  27021  clwlksfclwwlk  27049  1pthon2v  27131  uhgr3cyclex  27160  n4cyclfrgr  27271  frgrwopreg  27303  2clwwlk2clwwlklem1  27327  numclwlk1lem2f1  27347  frgrreggt1  27380  frgrreg  27381  frgrregord013  27382  chintcli  28318  spansnss  28558  elspansn4  28560  chscllem4  28627  hoadddir  28791  adjmul  29079  kbass6  29108  spansncv2  29280  sumdmdii  29402  nexple  30199  bnj1417  31235  mclsind  31593  iprodefisumlem  31752  poseq  31878  btwndiff  32259  elicc3  32436  finminlem  32437  sdclem2  33668  clmgmOLD  33780  grpomndo  33804  zerdivemp1x  33876  lsmsat  34613  lsmcv2  34634  lcvat  34635  lsatcveq0  34637  lcvexchlem4  34642  lcvexchlem5  34643  islshpcv  34658  l1cvpat  34659  lshpkrlem6  34720  omlfh3N  34864  cvlsupr4  34950  cvlsupr5  34951  cvlsupr6  34952  2llnneN  35013  hlrelat3  35016  cvrval3  35017  cvrval4N  35018  cvrexchlem  35023  2atlt  35043  cvrat4  35047  atbtwnexOLDN  35051  atbtwnex  35052  athgt  35060  3dim1  35071  3dim2  35072  3dim3  35073  1cvratex  35077  llnle  35122  atcvrlln2  35123  atcvrlln  35124  2llnmat  35128  lplnle  35144  lplnnle2at  35145  lplnnlelln  35147  llncvrlpln2  35161  2llnjN  35171  lvoli2  35185  lvolnlelln  35188  lvolnlelpln  35189  4atlem10  35210  4atlem11  35213  4atlem12  35216  lplncvrlvol2  35219  2lplnj  35224  lneq2at  35382  lnatexN  35383  lnjatN  35384  lncvrat  35386  2lnat  35388  cdlemb  35398  paddasslem14  35437  llnexchb2  35473  dalawlem10  35484  dalawlem13  35487  dalawlem14  35488  dalaw  35490  pclclN  35495  pclfinN  35504  osumcllem11N  35570  lhp2lt  35605  lhpexle3lem  35615  4atexlem7  35679  ldilcnv  35719  ldilco  35720  ltrncnv  35750  trlval2  35768  cdleme24  35957  cdleme26ee  35965  cdleme28  35978  cdleme32le  36052  cdleme50trn2  36156  cdleme50ltrn  36162  cdleme  36165  cdlemf1  36166  cdlemf  36168  cdlemg1cex  36193  cdlemg2ce  36197  cdlemg18b  36284  ltrnco  36324  tendocan  36429  cdlemk28-3  36513  cdlemk11t  36551  dia2dimlem6  36675  dia2dimlem12  36681  dihlsscpre  36840  dihord4  36864  dihord5b  36865  dihmeetlem3N  36911  dihmeetlem20N  36932  dvh4dimlem  37049  lclkrlem2y  37137  mapdpglem24  37310  mapdpglem32  37311  mapdpg  37312  baerlem3lem2  37316  baerlem5alem2  37317  baerlem5blem2  37318  mapdh9a  37396  mapdh9aOLDN  37397  hdmap14lem6  37482  hdmapglem7  37538  mzpexpmpt  37625  pellexlem5  37714  pellex  37716  pell14qrexpclnn0  37747  pellfundex  37767  monotuz  37823  monotoddzzfi  37824  expmordi  37829  rmxypos  37831  jm2.17a  37844  jm2.17b  37845  rmygeid  37848  jm2.19lem3  37875  jm2.15nn0  37887  jm2.16nn0  37888  aomclem2  37942  aomclem6  37946  dfac11  37949  hbtlem5  38015  cnsrexpcl  38052  relexpxpnnidm  38312  relexpiidm  38313  relexpss1d  38314  iunrelexpmin1  38317  relexpmulnn  38318  iunrelexpmin2  38321  relexp01min  38322  relexp0a  38325  relexpxpmin  38326  relexpaddss  38327  trclimalb2  38335  3impexpbicomi  39003  ee333  39030  eel12131  39255  eel2122old  39260  e333  39277  ordelordALTVD  39417  refsumcn  39503  uzwo4  39535  ssinc  39578  ssdec  39579  iunincfi  39586  restuni3  39615  eliuniin2  39617  rabssd  39646  reximdd  39658  suprnmpt  39669  wessf1ornlem  39685  disjf1o  39692  fompt  39693  disjinfi  39694  ssnnf1octb  39696  mapsnd  39702  choicefi  39706  mapssbi  39719  unirnmapsn  39720  ssmapsn  39722  iunmapsn  39723  funimassd  39745  rnmptlb  39767  rnmptbddlem  39769  fvelimad  39772  infnsuprnmpt  39779  fperiodmullem  39831  upbdrech  39833  ssfiunibd  39837  supxrgere  39862  iuneqfzuzlem  39863  supxrgelem  39866  supxrge  39867  suplesup  39868  infrpge  39880  infleinf  39901  suplesup2  39905  supxrunb3  39936  infleinf2  39954  rexabslelem  39958  infrnmptle  39963  infxrunb3rnmpt  39968  iccshift  40062  iooshift  40066  fmul01  40130  fmuldfeq  40133  fmul01lt1  40136  mullimc  40166  islptre  40169  mullimcf  40173  limcperiod  40178  islpcn  40189  limsupre  40191  limcleqr  40194  neglimc  40197  addlimc  40198  0ellimcdiv  40199  limclner  40201  fnlimfvre  40224  limsuppnflem  40260  limsupmnfuzlem  40276  limsupre3lem  40282  limsupre3uzlem  40285  climuzlem  40293  limsupgtlem  40327  coskpi2  40395  cosknegpi  40398  cncfshift  40405  cncfperiod  40410  icccncfext  40418  dvnmptdivc  40471  dvnmptconst  40474  dvnmul  40476  dvmptfprodlem  40477  dvmptfprod  40478  dvnprodlem1  40479  dvnprodlem2  40480  iblspltprt  40507  itgspltprt  40513  itgperiod  40515  ismbl3  40521  stoweidlem3  40538  stoweidlem31  40566  stoweidlem59  40594  stirlinglem13  40621  fourierdlem41  40683  fourierdlem42  40684  fourierdlem48  40689  fourierdlem51  40692  fourierdlem53  40694  fourierdlem70  40711  fourierdlem71  40712  fourierdlem73  40714  fourierdlem80  40721  fourierdlem81  40722  fourierdlem89  40730  fourierdlem91  40732  fourierdlem93  40734  fourierdlem97  40738  elaa2  40769  qndenserrnopnlem  40835  salexct  40870  subsaliuncl  40894  subsalsal  40895  sge0tsms  40915  sge0f1o  40917  sge0fsum  40922  sge0supre  40924  sge0sup  40926  sge0rnbnd  40928  sge0gerp  40930  sge0pnffigt  40931  sge0lefi  40933  sge0ltfirp  40935  sge0resrn  40939  sge0resplit  40941  sge0split  40944  sge0iunmptlemfi  40948  sge0iunmptlemre  40950  sge0iunmpt  40953  sge0rpcpnf  40956  sge0isum  40962  sge0xp  40964  sge0xaddlem2  40969  sge0uzfsumgt  40979  sge0seq  40981  sge0reuz  40982  nnfoctbdjlem  40990  nnfoctbdj  40991  iundjiun  40995  meadjiunlem  41000  voliunsge0lem  41007  meaiuninclem  41015  meaiininc2  41023  carageniuncllem1  41056  carageniuncllem2  41057  caratheodorylem1  41061  caratheodorylem2  41062  isomenndlem  41065  ovnsupge0  41092  ovnlerp  41097  ovncvrrp  41099  ovnsubaddlem1  41105  hoidmvval0  41122  hoidmv1lelem3  41128  hoidmv1le  41129  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  ovnhoilem2  41137  opnvonmbllem2  41168  ovolval5lem3  41189  ovnovollem3  41193  vonioo  41217  vonicc  41220  pimiooltgt  41242  sssmf  41268  smfaddlem1  41292  smflimlem6  41305  smfmullem4  41322  smfpimbor1lem1  41326  smfco  41330  smfpimcc  41335  smflimmpt  41337  smfinflem  41344  smflimsuplem7  41353  smflimsuplem8  41354  smflimsupmpt  41356  smfliminfmpt  41359  iccpartiltu  41683  goldbachth  41784  fmtnofac1  41807  prmdvdsfmtnof1lem1  41821  pwdif  41826  lighneal  41853  sprsymrelfvlem  42065  uspgropssxp  42077  rngccatidALTV  42314  ringccatidALTV  42377  nzerooringczr  42397  lcosslsp  42552  fllog2  42687  dignn0flhalf  42737  iunord  42747  setrec2fun  42764
  Copyright terms: Public domain W3C validator