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

Theorem 3exp 1111
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
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213expa 1110 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
32exp31 420 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  3expb  1112  3expib  1114  3com12  1115  3com13  1116  pm3.2an3  1332  3exp1  1344  3expd  1345  exp5o  1347  3ecase  1465  rexlimdv3a  3286  rabssdv  4050  reupick2  4288  disjiund  5048  otiunsndisj  5402  wefrc  5543  predpo  6160  tz7.7  6211  unizlim  6301  fvelimad  6726  fveqdmss  6839  f1oiso2  7094  ssorduni  7488  suceloni  7516  tfisi  7561  funeldmdif  7738  poxp  7813  smo11  7992  tfrlem5  8007  odi  8195  omass  8196  nndi  8239  nnmass  8240  undifixp  8487  findcard  8746  ac6sfi  8751  domunfican  8780  mapfien2  8861  fisup2g  8921  fiinf2g  8953  indcardi  9456  acndom  9466  ackbij1lem16  9646  infpssrlem4  9717  fin23lem11  9728  isfin2-2  9730  fin23lem34  9757  fin1a2lem10  9820  hsmexlem2  9838  axcc3  9849  domtriomlem  9853  axdc3lem2  9862  axdc3lem4  9864  axcclem  9868  ttukeyg  9928  axdclem2  9931  axacndlem4  10021  axacndlem5  10022  axacnd  10023  tskr1om2  10179  tskwe2  10184  tskord  10191  tskcard  10192  tskuni  10194  tskwun  10195  gruiin  10221  grudomon  10228  gruina  10229  mulcanpi  10311  adderpq  10367  mulerpq  10368  dedekindle  10793  divgt0  11497  divge0  11498  nnne0  11660  uzind  12063  uzind2  12064  iccsplit  12861  ssnn0fi  13343  expmordi  13521  sqlecan  13561  modexp  13589  expnngt1  13592  facavg  13651  2cshwcshw  14177  relexpcnv  14384  relexpreld  14389  relexpaddnn  14400  relexpaddg  14402  pwdif  15213  prodfn0  15240  prodfrec  15241  ntrivcvgfvn0  15245  fprodabs  15318  bpolycl  15396  bpolydif  15399  fprodefsum  15438  dvdsmodexp  15605  dvdsaddre2b  15647  dvdsnprmd  16024  2mulprm  16027  prmndvdsfaclt  16057  ncoprmlnprm  16058  fermltl  16111  pceu  16173  setsstruct2  16511  setsstruct  16513  mreexexd  16909  isglbd  17717  pmtrfrn  18517  psgnunilem4  18556  ablsimpgprmd  19168  mulgass2  19282  islss4  19665  lspsneu  19826  lspfixed  19831  lspexch  19832  lsmcv  19844  lspsolvlem  19845  xrsdsreclblem  20521  isphld  20728  mdetralt  21147  mdetunilem9  21159  fiinopn  21439  neips  21651  tpnei  21659  neindisj2  21661  opnneiid  21664  hausnei2  21891  cmpsublem  21937  cmpsub  21938  cmpcld  21940  comppfsc  22070  filufint  22458  cfinufil  22466  rnelfm  22491  alexsubALTlem1  22585  alexsubALTlem4  22588  alexsubALT  22589  tsmsxp  22692  neibl  23040  tngngp3  23194  tgqioo  23337  ovolunlem2  24028  iunmbl2  24087  itg1le  24243  vieta1  24830  aannenlem2  24847  aalioulem3  24852  aalioulem4  24853  aaliou2  24858  wilthlem3  25575  bcmono  25781  gausslemma2dlem1a  25869  iscgrglt  26228  axcontlem7  26684  elntg2  26699  edglnl  26856  numedglnl  26857  ausgrumgri  26880  ausgrusgri  26881  usgrausgrb  26882  usgredg2vtxeuALT  26932  ushgredgedg  26939  ushgredgedgloop  26941  nbuhgr2vtx1edgb  27062  cusgrsize2inds  27163  upgrewlkle2  27316  wlkl1loop  27347  redwlk  27382  pthdivtx  27438  pthdadjvtx  27439  upgr2pthnlp  27441  upgrspthswlk  27447  clwlkl1loop  27492  wwlksnred  27598  wwlksnextbi  27600  elwwlks2ons3im  27661  umgrwwlks2on  27664  clwwlknwwlksn  27744  clwwlkinwwlk  27746  wwlksext2clwwlk  27764  1pthon2v  27860  uhgr3cyclex  27889  n4cyclfrgr  27998  frgrwopreg  28030  numclwwlk1lem2f1  28064  clwwlknonclwlknonf1o  28069  wlkl0  28074  frgrreggt1  28100  frgrreg  28101  frgrregord013  28102  chintcli  29036  spansnss  29276  elspansn4  29278  chscllem4  29345  hoadddir  29509  adjmul  29797  kbass6  29826  spansncv2  29998  sumdmdii  30120  nexple  31168  bnj1417  32211  lfuhgr2  32263  cusgredgex  32266  sat1el2xp  32524  fmlasuc  32531  satffunlem1lem1  32547  satffunlem2lem1  32549  mclsind  32715  iprodefisumlem  32870  poseq  32993  fpr3g  33020  frrlem10  33030  btwndiff  33386  elicc3  33563  finminlem  33564  sdclem2  34900  clmgmOLD  35012  grpomndo  35036  zerdivemp1x  35108  lsmsat  36026  lsmcv2  36047  lcvat  36048  lsatcveq0  36050  lcvexchlem4  36055  lcvexchlem5  36056  islshpcv  36071  l1cvpat  36072  lshpkrlem6  36133  omlfh3N  36277  cvlsupr4  36363  cvlsupr5  36364  cvlsupr6  36365  2llnneN  36427  hlrelat3  36430  cvrval3  36431  cvrval4N  36432  cvrexchlem  36437  2atlt  36457  cvrat4  36461  atbtwnexOLDN  36465  atbtwnex  36466  athgt  36474  3dim1  36485  3dim2  36486  3dim3  36487  1cvratex  36491  llnle  36536  atcvrlln2  36537  atcvrlln  36538  2llnmat  36542  lplnle  36558  lplnnle2at  36559  lplnnlelln  36561  llncvrlpln2  36575  2llnjN  36585  lvoli2  36599  lvolnlelln  36602  lvolnlelpln  36603  4atlem10  36624  4atlem11  36627  4atlem12  36630  lplncvrlvol2  36633  2lplnj  36638  lneq2at  36796  lnatexN  36797  lnjatN  36798  lncvrat  36800  2lnat  36802  cdlemb  36812  paddasslem14  36851  llnexchb2  36887  dalawlem10  36898  dalawlem13  36901  dalawlem14  36902  dalaw  36904  pclclN  36909  pclfinN  36918  osumcllem11N  36984  lhp2lt  37019  lhpexle3lem  37029  4atexlem7  37093  ldilcnv  37133  ldilco  37134  ltrncnv  37164  trlval2  37181  cdleme24  37370  cdleme26ee  37378  cdleme28  37391  cdleme32le  37465  cdleme50trn2  37569  cdleme50ltrn  37575  cdleme  37578  cdlemf1  37579  cdlemf  37581  cdlemg1cex  37606  cdlemg2ce  37610  cdlemg18b  37697  ltrnco  37737  tendocan  37842  cdlemk28-3  37926  cdlemk11t  37964  dia2dimlem6  38087  dia2dimlem12  38093  dihlsscpre  38252  dihord4  38276  dihord5b  38277  dihmeetlem3N  38323  dihmeetlem20N  38344  dvh4dimlem  38461  lclkrlem2y  38549  mapdpglem24  38722  mapdpglem32  38723  mapdpg  38724  baerlem3lem2  38728  baerlem5alem2  38729  baerlem5blem2  38730  mapdh9a  38807  mapdh9aOLDN  38808  hdmap14lem6  38891  hdmapglem7  38947  nnadddir  39043  nnmulcom  39045  nn0rppwr  39062  sn-addid2  39114  remulcand  39130  mzpexpmpt  39222  pellexlem5  39310  pellex  39312  pell14qrexpclnn0  39343  pellfundex  39363  monotuz  39418  monotoddzzfi  39419  rmxypos  39424  jm2.17a  39437  jm2.17b  39438  rmygeid  39441  jm2.19lem3  39468  jm2.15nn0  39480  jm2.16nn0  39481  aomclem2  39535  aomclem6  39539  dfac11  39542  hbtlem5  39608  cnsrexpcl  39645  relexpxpnnidm  39928  relexpiidm  39929  relexpss1d  39930  iunrelexpmin1  39933  relexpmulnn  39934  iunrelexpmin2  39937  relexp01min  39938  relexp0a  39941  relexpxpmin  39942  relexpaddss  39943  trclimalb2  39951  tfindsd  40444  3impexpbicomi  40694  ee333  40721  eel12131  40927  eel2122old  40932  e333  40947  ordelordALTVD  41081  refsumcn  41167  uzwo4  41195  ssinc  41233  ssdec  41234  iunincfi  41240  restuni3  41265  eliuniin2  41267  rabssd  41291  reximdd  41301  suprnmpt  41310  disjf1o  41332  fompt  41333  disjinfi  41334  ssnnf1octb  41336  choicefi  41343  mapssbi  41356  unirnmapsn  41357  ssmapsn  41359  iunmapsn  41360  funimassd  41377  rnmptlb  41394  rnmptbddlem  41395  infnsuprnmpt  41402  fperiodmullem  41450  upbdrech  41452  ssfiunibd  41456  supxrgere  41481  iuneqfzuzlem  41482  supxrgelem  41485  supxrge  41486  suplesup  41487  infrpge  41499  infleinf  41520  suplesup2  41524  supxrunb3  41552  infleinf2  41568  rexabslelem  41572  infrnmptle  41577  infxrunb3rnmpt  41582  iccshift  41674  iooshift  41678  fmul01  41741  fmuldfeq  41744  fmul01lt1  41747  mullimc  41777  islptre  41780  mullimcf  41784  limcperiod  41789  islpcn  41800  limsupre  41802  limcleqr  41805  neglimc  41808  addlimc  41809  0ellimcdiv  41810  limclner  41812  fnlimfvre  41835  limsuppnflem  41871  limsupmnfuzlem  41887  limsupre3lem  41893  limsupre3uzlem  41896  climuzlem  41904  limsupgtlem  41938  coskpi2  42027  cosknegpi  42030  cncfshift  42037  cncfperiod  42042  icccncfext  42050  dvnmptdivc  42103  dvnmptconst  42106  dvnmul  42108  dvmptfprodlem  42109  dvmptfprod  42110  dvnprodlem1  42111  dvnprodlem2  42112  iblspltprt  42138  itgspltprt  42144  itgperiod  42146  ismbl3  42152  stoweidlem3  42169  stoweidlem31  42197  stoweidlem59  42225  stirlinglem13  42252  fourierdlem41  42314  fourierdlem42  42315  fourierdlem48  42320  fourierdlem51  42323  fourierdlem53  42325  fourierdlem70  42342  fourierdlem71  42343  fourierdlem73  42345  fourierdlem80  42352  fourierdlem81  42353  fourierdlem89  42361  fourierdlem91  42363  fourierdlem93  42365  fourierdlem97  42369  elaa2  42400  qndenserrnopnlem  42463  salexct  42498  subsaliuncl  42522  subsalsal  42523  sge0tsms  42543  sge0f1o  42545  sge0fsum  42550  sge0supre  42552  sge0sup  42554  sge0rnbnd  42556  sge0gerp  42558  sge0pnffigt  42559  sge0lefi  42561  sge0ltfirp  42563  sge0resrn  42567  sge0resplit  42569  sge0split  42572  sge0iunmptlemfi  42576  sge0iunmptlemre  42578  sge0iunmpt  42581  sge0rpcpnf  42584  sge0isum  42590  sge0xp  42592  sge0xaddlem2  42597  sge0uzfsumgt  42607  sge0seq  42609  sge0reuz  42610  nnfoctbdjlem  42618  nnfoctbdj  42619  iundjiun  42623  meadjiunlem  42628  voliunsge0lem  42635  meaiuninclem  42643  meaiininc2  42651  carageniuncllem1  42684  carageniuncllem2  42685  caratheodorylem1  42689  caratheodorylem2  42690  isomenndlem  42693  ovnsupge0  42720  ovnlerp  42725  ovncvrrp  42727  ovnsubaddlem1  42733  hoidmvval0  42750  hoidmv1lelem3  42756  hoidmv1le  42757  hoidmvlelem1  42758  hoidmvlelem2  42759  hoidmvlelem3  42760  ovnhoilem2  42765  opnvonmbllem2  42796  ovolval5lem3  42817  ovnovollem3  42821  vonioo  42845  vonicc  42848  pimiooltgt  42870  sssmf  42896  smfaddlem1  42920  smflimlem6  42933  smfmullem4  42950  smfpimbor1lem1  42954  smfco  42958  smfpimcc  42963  smflimmpt  42965  smfinflem  42972  smflimsuplem7  42981  smflimsuplem8  42982  smflimsupmpt  42984  smfliminfmpt  42987  iccpartiltu  43429  sprsymrelfvlem  43499  reuopreuprim  43535  goldbachth  43556  fmtnofac1  43579  prmdvdsfmtnof1lem1  43593  lighneal  43623  isomgrsym  43848  isomgrtr  43851  uspgropssxp  43866  rngccatidALTV  44158  ringccatidALTV  44221  nzerooringczr  44241  lcosslsp  44391  fllog2  44526  dignn0flhalf  44576  itschlc0yqe  44645  itsclc0xyqsol  44653  iunord  44677  setrec2fun  44693
  Copyright terms: Public domain W3C validator