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

Theorem mpan9 510
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 34 . 2 (𝜒 → (𝜑𝜃))
43impcom 411 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  sylan  583  vtocl2gf  3545  vtocl3gf  3546  vtocl2g  3547  vtoclegft  3557  sbcthdv  3763  elinsn  4620  axprlem4  5304  swopolem  5460  wereu  5528  funssres  6377  dffv2  6738  fmptcof  6874  fnprb  6953  fntpb  6954  fliftfuns  7051  isorel  7063  oveqrspc2v  7167  caovclg  7325  caovcomg  7328  caovassg  7331  caovcang  7334  caovordig  7338  caovordg  7340  caovdig  7347  caovdirg  7350  peano5  7590  fvmpocurryd  7924  qliftfuns  8371  nneneq  8688  cfslb  9677  hsmexlem4  9840  axdc3lem2  9862  axdc4lem  9866  adderpq  10367  mulerpq  10368  ltordlem  11154  lble  11580  uz11  12255  xrsupsslem  12688  xrinfmsslem  12689  xrsupss  12690  xrinfmss  12691  fseqsupubi  13341  hashbclem  13806  ccatass  13933  swrdswrd  14058  swrdccatin1  14078  swrdccatin2  14082  cshwcsh2id  14181  wwlktovf  14311  isercolllem1  15012  caucvgb  15027  zsum  15066  fsum  15068  fsumf1o  15071  fsumcvg2  15075  isummulc2  15108  fsum2dlem  15116  fsumcom2  15120  fsumshftm  15127  fsum0diag2  15129  fsum00  15144  fsumrlim  15157  o1fsum  15159  isumshft  15185  clim2prod  15235  ntrivcvgfvn0  15246  zprod  15282  fprod  15286  fprodf1o  15291  prodss  15292  fprodser  15294  fprodcllemf  15303  fprodm1s  15315  fprodp1s  15316  fprodabs  15319  fprod2dlem  15325  fprodcom2  15329  fprodefsum  15439  mod2eq1n2dvds  15687  sumeven  15727  lcmfun  15978  pythagtriplem4  16145  pcmptdvds  16219  prslem  17532  posi  17551  dlatmjdi  17795  lidrididd  17871  grpidinv2  18149  ghmlin  18354  cntzmhm2  18461  dprdss  19142  dprd2d2  19157  srgrz  19267  srglz  19268  ringinvnz1ne0  19336  lmodlema  19630  islmodd  19631  lsscl  19705  lsslss  19724  lspdisjb  19889  rrgeq0i  20053  lsslinds  20518  assalem  20544  fvmptnn04if  21452  chfacfscmulgsum  21463  chfacfpmmulgsum  21467  ssnei2  21719  t1ficld  21930  t1sep2  21972  unconn  22032  1stcclb  22047  ptbasfi  22184  tx1stc  22253  qtoptop2  22302  r0sep  22351  ustincl  22811  ustdiag  22812  ustinvel  22813  ustexhalf  22814  psmet0  22913  psmettri2  22914  prdsdsf  22972  prdsxmet  22974  cncfi  23497  ovolfiniun  24103  mbfimaopnlem  24257  limciun  24495  dvcn  24522  dvmptfsum  24576  dvfsumle  24622  dvfsumabs  24624  dvfsumlem3  24629  itgsubst  24650  fsumvma  25795  dchrelbasd  25821  dchrisumlem3  26073  axcontlem9  26764  usgruspgrb  26972  uspgrloopvtxel  27304  umgr2v2evtxel  27310  clwwlknonex2lem2  27891  3spthd  27959  grpoass  28284  lnolin  28535  elnlfn  29709  strlem4  30035  hstrlem4  30043  atmd  30180  nn0min  30546  omndadd  30738  slmdlema  30862  qsxpid  30959  esumcvg  31419  measxun2  31543  sibfima  31670  bnj110  32204  bnj594  32258  bnj1491  32403  loop1cycl  32458  cvmcov  32584  mrsubcn  32840  dfon2lem5  33106  sssslt1  33334  madeval2  33364  ifscgr  33579  nn0prpw  33745  neibastop2lem  33782  bj-restb  34470  poimirlem25  35041  poimirlem32  35048  mbfresfi  35062  totbndss  35174  ghomlinOLD  35285  rngodi  35301  rngodir  35302  rngoass  35303  rngohomadd  35366  rngohommul  35367  crngocom  35398  idladdcl  35416  idllmulcl  35417  idlrmulcl  35418  exlimddvf  35518  oposlem  36437  cvlexch1  36583  hlsuprexch  36636  lautle  37339  elrfirn2  39568  wepwsolem  39917  kelac1  39938  islssfg2  39946  lnmlssfg  39955  2elfz3nn0  43813  2elfz2melfz  43815  icceuelpartlem  43892  wtgoldbnnsum4prm  44260  bgoldbnnsum3prm  44262  bgoldbtbnd  44267  setrec2fun  45162
  Copyright terms: Public domain W3C validator