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

Theorem mpan9 485
 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 445 1 ((𝜑𝜒) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  sylan  487  vtocl2gf  3241  vtocl3gf  3242  vtoclegft  3253  sbcthdv  3418  swopolem  4968  wereu  5034  funssres  5844  dffv2  6181  fmptcof  6304  fnprb  6377  fntpb  6378  fliftfuns  6464  isorel  6476  oveqrspc2v  6572  caovclg  6724  caovcomg  6727  caovassg  6730  caovcang  6733  caovordig  6737  caovordg  6739  caovdig  6746  caovdirg  6749  peano5  6981  fvmpt2curryd  7284  qliftfuns  7721  nneneq  8028  cfslb  8971  hsmexlem4  9134  axdc3lem2  9156  axdc4lem  9160  adderpq  9657  mulerpq  9658  ltordlem  10432  lble  10854  uz11  11586  xrsupsslem  12009  xrinfmsslem  12010  xrsupss  12011  xrinfmss  12012  fseqsupubi  12639  hashbclem  13093  swrdswrd  13312  swrdccatin2  13338  cshwcsh2id  13425  wwlktovf  13547  isercolllem1  14243  caucvgb  14258  zsum  14296  fsum  14298  fsumf1o  14301  fsumcvg2  14305  isummulc2  14335  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  fsumshftm  14355  fsum0diag2  14357  fsum00  14371  fsumrlim  14384  o1fsum  14386  isumshft  14410  clim2prod  14459  ntrivcvgfvn0  14470  zprod  14506  fprod  14510  fprodf1o  14515  prodss  14516  fprodser  14518  fprodm1s  14539  fprodp1s  14540  fprodabs  14543  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  fprodefsum  14664  mod2eq1n2dvds  14909  sumeven  14948  lcmfun  15196  dvdsprm  15253  pythagtriplem4  15362  pcmptdvds  15436  prslem  16754  posi  16773  dlatmjdi  17017  grpidinv2  17297  ghmlin  17488  cntzmhm2  17595  dprdss  18251  dprd2d2  18266  srgrz  18349  srglz  18350  ringinvnz1ne0  18415  lmodlema  18691  islmodd  18692  lsscl  18764  lsslss  18782  lspdisjb  18947  rrgeq0i  19110  assalem  19137  lsslinds  19989  fvmptnn04if  20473  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  ssnei2  20730  t1ficld  20941  t1sep2  20983  uncon  21042  1stcclb  21057  ptbasfi  21194  tx1stc  21263  qtoptop2  21312  r0sep  21361  ustincl  21821  ustdiag  21822  ustinvel  21823  ustexhalf  21824  psmet0  21923  psmettri2  21924  prdsdsf  21982  prdsxmet  21984  cncfi  22505  ovolfiniun  23076  mbfimaopnlem  23228  limciun  23464  dvcn  23490  dvmptfsum  23542  dvfsumle  23588  dvfsumabs  23590  dvfsumlem3  23595  itgsubst  23616  fsumvma  24738  dchrelbasd  24764  dchrisumlem3  24980  axcontlem9  25652  usgranloop0  25909  nbgrassovt  25964  usgra2wlkspthlem2  26148  4cycl4dv  26195  numclwwlkovf2ex  26613  grpoass  26741  lnolin  26993  elnlfn  28171  strlem4  28497  hstrlem4  28505  atmd  28642  nn0min  28954  omndadd  29037  slmdlema  29087  esumcvg  29475  measxun2  29600  sibfima  29727  bnj110  30182  bnj594  30236  bnj1491  30379  cvmcov  30499  mrsubcn  30670  dfon2lem5  30936  frrlem4  31027  nofulllem5  31105  ifscgr  31321  nn0prpw  31488  neibastop2lem  31525  bj-restb  32228  poimirlem25  32604  poimirlem32  32611  mbfresfi  32626  totbndss  32746  ghomlinOLD  32857  rngodi  32873  rngodir  32874  rngoass  32875  rngohomadd  32938  rngohommul  32939  crngocom  32970  idladdcl  32988  idllmulcl  32989  idlrmulcl  32990  exlimddvf  33096  oposlem  33487  cvlexch1  33633  hlsuprexch  33685  lautle  34388  elrfirn2  36277  wepwsolem  36630  kelac1  36651  islssfg2  36659  lnmlssfg  36668  icceuelpartlem  39973  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  bgoldbtbnd  40225  2elfz3nn0  40353  2elfz2melfz  40355  usgruspgrb  40411  uspgrloopvtxel  40732  umgr2v2evtxel  40738  3spthd  41343  av-numclwwlkovf2ex  41517  setrec2fun  42238
 Copyright terms: Public domain W3C validator