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

Theorem exp31 627
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp31.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
exp31 (𝜑 → (𝜓 → (𝜒𝜃)))

Proof of Theorem exp31
StepHypRef Expression
1 exp31.1 . . 3 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
21ex 448 . 2 ((𝜑𝜓) → (𝜒𝜃))
32ex 448 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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
This theorem is referenced by:  exp41  635  exp42  636  expl  645  exbiri  649  anasss  676  an31s  843  pm3.2an3  1232  3impa  1250  exp516  1278  r19.29af2  3056  reusv2lem2  4789  pwssun  4933  onmindif  5717  mpteqb  6191  dffo3  6266  fliftfun  6439  elovmpt3rab1  6768  ordsucss  6887  tfindsg  6929  imacosupp  7199  tfrlem1  7336  tfrlem9  7345  oaordi  7490  oaordex  7502  oaass  7505  oarec  7506  omlimcl  7522  omass  7524  oen0  7530  oeordsuc  7538  nnaordi  7562  omsmolem  7597  infensuc  8000  php3  8008  marypha1lem  8199  hartogs  8309  card2on  8319  tz9.12lem3  8512  infxpenlem  8696  cfflb  8941  cfcoflem  8954  cfcof  8956  isf32lem12  9046  zorn2lem6  9183  ondomon  9241  alephval2  9250  pwcfsdom  9261  axrepnd  9272  fpwwe2lem12  9319  genpcd  9684  ltexprlem6  9719  recexsr  9784  axpre-sup  9846  negf1o  10311  recex  10510  zdiv  11281  uzaddcl  11578  nn01to3  11615  rpnnen1lem5  11652  rpnnen1lem5OLD  11658  xrsupsslem  11967  xrinfmsslem  11968  supxrunb1  11979  supxrunb2  11980  fz0fzelfz0  12271  fz0fzdiffz0  12274  elfzmlbp  12276  difelfzle  12278  fzo1fzo0n0  12343  elincfzoext  12350  ssfzo12bi  12386  elfznelfzo  12396  modaddmodup  12552  modfzo0difsn  12561  fsuppmapnn0fiubex  12611  seqf1o  12661  expcllem  12690  expeq0  12709  mulexp  12718  hashgt12el2  13025  hashimarni  13040  hash2prd  13066  fi1uzind  13082  fi1uzindOLD  13088  swrdnd  13232  swrdswrdlem  13259  swrdswrd  13260  swrdccat3  13291  swrdccatid  13296  repswswrd  13330  repswccat  13331  cshwidxmod  13348  2cshwcshw  13370  s4f1o  13461  wwlktovfo  13497  cjexp  13686  resqrex  13787  absexp  13840  summo  14243  fsum2d  14292  modfsummods  14314  binom  14349  clim2prod  14407  fprod2d  14498  binomfallfac  14559  efexp  14618  demoivreALT  14718  divconjdvds  14823  addmodlteqALT  14833  dfgcd2  15049  lcmfunsnlem2lem1  15137  lcmfdvdsb  15142  lcmfun  15144  coprmprod  15161  coprmproddvdslem  15162  oddprmdvds  15393  ramcl  15519  cshwsidrepswmod0  15587  cshwshashlem1  15588  ressress  15713  initoeu2lem1  16435  symggen  17661  pmtr3ncom  17666  srgmulgass  18302  srgbinom  18316  ringinvnzdiv  18364  lmodvsmmulgdi  18669  assamulgscmlem2  19118  mptcoe1fsupp  19354  coe1fzgsumdlem  19440  evl1gsumdlem  19489  psgndiflemB  19712  scmatmulcl  20090  mdetdiagid  20172  pm2mpf1  20370  mptcoe1matfsupp  20373  mp2pm2mplem4  20380  chpdmat  20412  chfacfisf  20425  chfacfisfcpmat  20426  chcoeffeq  20457  topbas  20534  fctop  20565  cctop  20567  elcls  20634  elcls3  20644  2ndcdisj  21016  filufint  21481  ovoliunlem3  23023  dvge0  23517  ulmcn  23901  gausslemma2dlem3  24837  usgrares1  25732  cusgrarn  25781  cusgrares  25794  usgrasscusgra  25804  pthdepisspth  25897  usgra2adedgspthlem2  25933  usgra2wlkspthlem1  25940  usgra2wlkspth  25942  fargshiftf1  25958  usgrcyclnl2  25962  constr3trllem2  25972  wlkiswwlk1  26011  wwlknred  26044  wwlkextinj  26051  wwlkextproplem2  26063  0clwlk  26086  clwlkisclwwlklem2a4  26105  clwlkisclwwlklem2a  26106  clwlkisclwwlklem1  26108  clwwlkf  26115  clwwlkf1  26117  wwlkext2clwwlk  26124  clwwisshclww  26128  erclwwlktr  26136  clwwlknscsh  26140  usg2cwwk2dif  26141  erclwwlkntr  26148  clwlkfclwwlk  26164  clwlkf1clwwlklem  26169  usg2wotspth  26204  usgfidegfi  26230  usgravd00  26239  eupatrl  26288  2pthfrgra  26331  3cyclfrgrarn1  26332  3cyclfrgrarn  26333  frgrancvvdeq  26362  frgrancvvdgeq  26363  frgrawopreglem5  26368  usg2spot2nb  26385  extwwlkfablem1  26394  extwwlkfablem2  26398  numclwwlkovf2ex  26406  numclwlk1lem2foa  26411  numclwlk1lem2fo  26415  numclwlk2lem2f  26423  numclwlk2lem2f1o  26425  frgrareggt1  26436  frgrareg  26437  friendshipgt3  26441  friendship  26442  grpoinvf  26563  nmosetre  26796  ipasslem1  26863  shmodsi  27425  elspansn5  27610  normcan  27612  h1datomi  27617  nmopsetretALT  27899  nmfnsetre  27913  pjss2coi  28200  pj3cor1i  28245  mdexchi  28371  superpos  28390  atcvat4i  28433  mdsymlem3  28441  mdsymlem4  28442  sumdmdii  28451  cdj3lem2b  28473  elabreximd  28525  iuninc  28554  iundisjf  28577  xrsmulgzz  28802  gsumle  28903  gsumvsca1  28906  gsumvsca2  28907  ofldchr  28938  locfinreflem  29028  xrge0iifiso  29102  lmxrge0  29119  esumfzf  29251  sigaclfu2  29304  eulerpartlemgh  29560  signstfvneq0  29768  signstfvc  29770  bccolsum  30671  faclimlem1  30675  dftrpred3g  30770  segletr  31184  segleantisym  31185  outsideoftr  31199  exp5d  31259  elicc3  31274  finxpreclem2  32186  wl-sbcom2d  32306  poimirlem26  32388  mblfinlem3  32401  itg2addnc  32417  indexa  32481  ax12indalem  33031  ax12inda2ALT  33032  cvrat4  33530  elpaddn0  33887  paddasslem5  33911  paddasslem14  33920  eldioph2  36126  pell1234qrdich  36226  gneispb  37232  dffo3f  38142  climsuselem1  38457  stoweidlem19  38695  stoweidlem20  38696  stoweidlem34  38710  wallispilem3  38743  sge0iunmpt  39094  smflimlem4  39443  iccpartigtl  39745  iccpartgt  39749  icceuelpartlem  39757  lighneallem3  39846  gbogt5  39968  bgoldbtbndlem3  40007  bgoldbtbndlem4  40008  bgoldbtbnd  40009  tgblthelfgott  40013  tgblthelfgottOLD  40020  pfxccat3  40073  2elfz2melfz  40161  subsubelfzo0  40165  sizusglecusg  40660  upgr1wlkwlk  40828  2pthnloop  40918  crctcsh1wlkn0  41005  wwlksnred  41079  wwlksnextinj  41086  wwlksnextproplem2  41097  wwlksnextproplem3  41098  wwlks2onv  41139  usgr2wspthons3  41148  clwlkclwwlklem2a4  41187  clwlkclwwlklem2a  41188  clwlkclwwlklem2  41190  clwwlksf  41203  clwwlksf1  41205  wwlksext2clwwlk  41212  erclwwlkstr  41224  clwwlksnscsh  41228  umgr2cwwk2dif  41229  erclwwlksntr  41236  clwlksfclwwlk  41250  clwlksf1clwwlklem  41256  uhgr3cyclex  41330  upgr4cycl4dv4e  41333  eucrctshift  41392  3cyclfrgrrn1  41436  frgrncvvdeqlemC  41459  frgrwopreglem5  41466  av-extwwlkfablem2  41491  av-numclwwlkovf2ex  41498  av-numclwlk1lem2foa  41502  av-numclwlk1lem2fo  41506  av-numclwlk2lem2f  41514  av-numclwlk2lem2f1o  41516  av-frgrareg  41529  av-friendshipgt3  41533  av-friendship  41534  2zrngagrp  41714  rhmsubcrngclem2  41801  nzerooringczr  41845  lmodvsmdi  41938  ply1mulgsumlem1  41949  islindeps2  42047  elfzolborelfzop1  42084  nnolog2flm1  42163  nn0sumshdiglemA  42192
  Copyright terms: Public domain W3C validator