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

Theorem mpan9 507
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 408 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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
This theorem is referenced by:  sylan  580  vtocl2gf  3570  vtocl3gf  3571  vtocl2g  3572  vtoclegft  3582  sbcthdv  3787  elinsn  4640  axprlem4  5318  swopolem  5477  wereu  5545  funssres  6392  dffv2  6750  fmptcof  6885  fnprb  6963  fntpb  6964  fliftfuns  7056  isorel  7068  oveqrspc2v  7172  caovclg  7329  caovcomg  7332  caovassg  7335  caovcang  7338  caovordig  7342  caovordg  7344  caovdig  7351  caovdirg  7354  peano5  7593  fvmpocurryd  7928  qliftfuns  8374  nneneq  8689  cfslb  9677  hsmexlem4  9840  axdc3lem2  9862  axdc4lem  9866  adderpq  10367  mulerpq  10368  ltordlem  11154  lble  11582  uz11  12256  xrsupsslem  12690  xrinfmsslem  12691  xrsupss  12692  xrinfmss  12693  fseqsupubi  13336  hashbclem  13800  ccatass  13932  swrdswrd  14057  swrdccatin1  14077  swrdccatin2  14081  cshwcsh2id  14180  wwlktovf  14310  isercolllem1  15011  caucvgb  15026  zsum  15065  fsum  15067  fsumf1o  15070  fsumcvg2  15074  isummulc2  15107  fsum2dlem  15115  fsumcom2  15119  fsumshftm  15126  fsum0diag2  15128  fsum00  15143  fsumrlim  15156  o1fsum  15158  isumshft  15184  clim2prod  15234  ntrivcvgfvn0  15245  zprod  15281  fprod  15285  fprodf1o  15290  prodss  15291  fprodser  15293  fprodcllemf  15302  fprodm1s  15314  fprodp1s  15315  fprodabs  15318  fprod2dlem  15324  fprodcom2  15328  fprodefsum  15438  mod2eq1n2dvds  15686  sumeven  15728  lcmfun  15979  pythagtriplem4  16146  pcmptdvds  16220  prslem  17531  posi  17550  dlatmjdi  17794  lidrididd  17870  grpidinv2  18098  ghmlin  18303  cntzmhm2  18410  dprdss  19082  dprd2d2  19097  srgrz  19207  srglz  19208  ringinvnz1ne0  19273  lmodlema  19570  islmodd  19571  lsscl  19645  lsslss  19664  lspdisjb  19829  rrgeq0i  19992  assalem  20019  lsslinds  20905  fvmptnn04if  21387  chfacfscmulgsum  21398  chfacfpmmulgsum  21402  ssnei2  21654  t1ficld  21865  t1sep2  21907  unconn  21967  1stcclb  21982  ptbasfi  22119  tx1stc  22188  qtoptop2  22237  r0sep  22286  ustincl  22745  ustdiag  22746  ustinvel  22747  ustexhalf  22748  psmet0  22847  psmettri2  22848  prdsdsf  22906  prdsxmet  22908  cncfi  23431  ovolfiniun  24031  mbfimaopnlem  24185  limciun  24421  dvcn  24447  dvmptfsum  24501  dvfsumle  24547  dvfsumabs  24549  dvfsumlem3  24554  itgsubst  24575  fsumvma  25717  dchrelbasd  25743  dchrisumlem3  25995  axcontlem9  26686  usgruspgrb  26894  uspgrloopvtxel  27226  umgr2v2evtxel  27232  clwwlknonex2lem2  27815  3spthd  27883  grpoass  28208  lnolin  28459  elnlfn  29633  strlem4  29959  hstrlem4  29967  atmd  30104  nn0min  30464  omndadd  30635  slmdlema  30759  qsxpid  30855  esumcvg  31245  measxun2  31369  sibfima  31496  bnj110  32030  bnj594  32084  bnj1491  32227  loop1cycl  32282  cvmcov  32408  mrsubcn  32664  dfon2lem5  32930  sssslt1  33158  madeval2  33188  ifscgr  33403  nn0prpw  33569  neibastop2lem  33606  bj-restb  34280  poimirlem25  34799  poimirlem32  34806  mbfresfi  34820  totbndss  34938  ghomlinOLD  35049  rngodi  35065  rngodir  35066  rngoass  35067  rngohomadd  35130  rngohommul  35131  crngocom  35162  idladdcl  35180  idllmulcl  35181  idlrmulcl  35182  exlimddvf  35282  oposlem  36200  cvlexch1  36346  hlsuprexch  36399  lautle  37102  elrfirn2  39173  wepwsolem  39522  kelac1  39543  islssfg2  39551  lnmlssfg  39560  2elfz3nn0  43397  2elfz2melfz  43399  icceuelpartlem  43442  wtgoldbnnsum4prm  43814  bgoldbnnsum3prm  43816  bgoldbtbnd  43821  setrec2fun  44693
  Copyright terms: Public domain W3C validator