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

Theorem mpan9 484
Description: Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Hypotheses
Ref Expression
mpan9.1 (𝜑𝜓)
mpan9.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
mpan9 ((𝜑𝜒) → 𝜃)

Proof of Theorem mpan9
StepHypRef Expression
1 mpan9.1 . . 3 (𝜑𝜓)
2 mpan9.2 . . 3 (𝜒 → (𝜓𝜃))
31, 2syl5 33 . 2 (𝜒 → (𝜑𝜃))
43impcom 444 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:  sylan  486  vtocl2gf  3240  vtocl3gf  3241  vtoclegft  3252  sbcthdv  3417  swopolem  4958  wereu  5024  funssres  5830  dffv2  6166  fmptcof  6289  fnprb  6355  fntpb  6356  fliftfuns  6442  isorel  6454  oveqrspc2v  6550  caovclg  6701  caovcomg  6704  caovassg  6707  caovcang  6710  caovordig  6714  caovordg  6716  caovdig  6723  caovdirg  6726  peano5  6958  fvmpt2curryd  7261  qliftfuns  7698  nneneq  8005  cfslb  8948  hsmexlem4  9111  axdc3lem2  9133  axdc4lem  9137  adderpq  9634  mulerpq  9635  ltordlem  10402  lble  10824  uz11  11542  xrsupsslem  11965  xrinfmsslem  11966  xrsupss  11967  xrinfmss  11968  fseqsupubi  12594  hashbclem  13045  swrdswrd  13258  swrdccatin2  13284  cshwcsh2id  13371  wwlktovf  13493  isercolllem1  14189  caucvgb  14204  zsum  14242  fsum  14244  fsumf1o  14247  fsumcvg2  14251  isummulc2  14281  fsum2dlem  14289  fsumcom2  14293  fsumcom2OLD  14294  fsumshftm  14301  fsum0diag2  14303  fsum00  14317  fsumrlim  14330  o1fsum  14332  isumshft  14356  clim2prod  14405  ntrivcvgfvn0  14416  zprod  14452  fprod  14456  fprodf1o  14461  prodss  14462  fprodser  14464  fprodm1s  14485  fprodp1s  14486  fprodabs  14489  fprod2dlem  14495  fprodcom2  14499  fprodcom2OLD  14500  fprodefsum  14610  mod2eq1n2dvds  14855  sumeven  14894  lcmfun  15142  dvdsprm  15199  pythagtriplem4  15308  pcmptdvds  15382  prslem  16700  posi  16719  dlatmjdi  16963  grpidinv2  17243  ghmlin  17434  cntzmhm2  17541  dprdss  18197  dprd2d2  18212  srgrz  18295  srglz  18296  ringinvnz1ne0  18361  lmodlema  18637  islmodd  18638  lsscl  18710  lsslss  18728  lspdisjb  18893  rrgeq0i  19056  assalem  19083  lsslinds  19931  fvmptnn04if  20415  chfacfscmulgsum  20426  chfacfpmmulgsum  20430  ssnei2  20672  t1ficld  20883  t1sep2  20925  uncon  20984  1stcclb  20999  ptbasfi  21136  tx1stc  21205  qtoptop2  21254  r0sep  21303  ustincl  21763  ustdiag  21764  ustinvel  21765  ustexhalf  21766  psmet0  21865  psmettri2  21866  prdsdsf  21923  prdsxmet  21925  cncfi  22436  ovolfiniun  22993  mbfimaopnlem  23145  limciun  23381  dvcn  23407  dvmptfsum  23459  dvfsumle  23505  dvfsumabs  23507  dvfsumlem3  23512  itgsubst  23533  fsumvma  24655  dchrelbasd  24681  dchrisumlem3  24897  axcontlem9  25570  usgranloop0  25675  nbgrassovt  25730  usgra2wlkspthlem2  25914  4cycl4dv  25961  numclwwlkovf2ex  26379  grpoass  26507  lnolin  26799  elnlfn  27977  strlem4  28303  hstrlem4  28311  atmd  28448  nn0min  28760  omndadd  28843  slmdlema  28893  esumcvg  29281  measxun2  29406  sibfima  29533  bnj110  29988  bnj594  30042  bnj1491  30185  cvmcov  30305  mrsubcn  30476  dfon2lem5  30742  frrlem4  30833  nofulllem5  30911  ifscgr  31127  nn0prpw  31294  neibastop2lem  31331  bj-restb  32024  poimirlem25  32400  poimirlem32  32407  mbfresfi  32422  totbndss  32542  ghomlinOLD  32653  rngodi  32669  rngodir  32670  rngoass  32671  rngohomadd  32734  rngohommul  32735  crngocom  32766  idladdcl  32784  idllmulcl  32785  idlrmulcl  32786  exlimddvf  32892  oposlem  33283  cvlexch1  33429  hlsuprexch  33481  lautle  34184  elrfirn2  36073  wepwsolem  36426  kelac1  36447  islssfg2  36455  lnmlssfg  36464  icceuelpartlem  39771  wtgoldbnnsum4prm  40016  bgoldbnnsum3prm  40018  bgoldbtbnd  40023  2elfz3nn0  40173  2elfz2melfz  40175  usgruspgrb  40406  uspgrloopvtxel  40727  umgr2v2evtxel  40733  3spthd  41338  av-numclwwlkovf2ex  41512
  Copyright terms: Public domain W3C validator