MPE Home 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 34 . 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 197  df-an 385
This theorem is referenced by:  sylan  487  vtocl2gf  3299  vtocl3gf  3300  vtoclegft  3311  sbcthdv  3484  elinsn  4277  swopolem  5073  wereu  5139  funssres  5968  dffv2  6310  fmptcof  6437  fnprb  6513  fntpb  6514  fliftfuns  6604  isorel  6616  oveqrspc2v  6713  caovclg  6868  caovcomg  6871  caovassg  6874  caovcang  6877  caovordig  6881  caovordg  6883  caovdig  6890  caovdirg  6893  peano5  7131  fvmpt2curryd  7442  qliftfuns  7877  nneneq  8184  cfslb  9126  hsmexlem4  9289  axdc3lem2  9311  axdc4lem  9315  adderpq  9816  mulerpq  9817  ltordlem  10591  lble  11013  uz11  11748  xrsupsslem  12175  xrinfmsslem  12176  xrsupss  12177  xrinfmss  12178  fseqsupubi  12817  hashbclem  13274  swrdswrd  13506  swrdccatin2  13533  cshwcsh2id  13620  wwlktovf  13745  isercolllem1  14439  caucvgb  14454  zsum  14493  fsum  14495  fsumf1o  14498  fsumcvg2  14502  isummulc2  14537  fsum2dlem  14545  fsumcom2  14549  fsumcom2OLD  14550  fsumshftm  14557  fsum0diag2  14559  fsum00  14574  fsumrlim  14587  o1fsum  14589  isumshft  14615  clim2prod  14664  ntrivcvgfvn0  14675  zprod  14711  fprod  14715  fprodf1o  14720  prodss  14721  fprodser  14723  fprodm1s  14744  fprodp1s  14745  fprodabs  14748  fprod2dlem  14754  fprodcom2  14758  fprodcom2OLD  14759  fprodefsum  14869  mod2eq1n2dvds  15118  sumeven  15157  lcmfun  15405  dvdsprm  15462  pythagtriplem4  15571  pcmptdvds  15645  prslem  16978  posi  16997  dlatmjdi  17241  grpidinv2  17521  ghmlin  17712  cntzmhm2  17818  dprdss  18474  dprd2d2  18489  srgrz  18572  srglz  18573  ringinvnz1ne0  18638  lmodlema  18916  islmodd  18917  lsscl  18991  lsslss  19009  lspdisjb  19174  rrgeq0i  19337  assalem  19364  lsslinds  20218  fvmptnn04if  20702  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  ssnei2  20968  t1ficld  21179  t1sep2  21221  unconn  21280  1stcclb  21295  ptbasfi  21432  tx1stc  21501  qtoptop2  21550  r0sep  21599  ustincl  22058  ustdiag  22059  ustinvel  22060  ustexhalf  22061  psmet0  22160  psmettri2  22161  prdsdsf  22219  prdsxmet  22221  cncfi  22744  ovolfiniun  23315  mbfimaopnlem  23467  limciun  23703  dvcn  23729  dvmptfsum  23783  dvfsumle  23829  dvfsumabs  23831  dvfsumlem3  23836  itgsubst  23857  fsumvma  24983  dchrelbasd  25009  dchrisumlem3  25225  axcontlem9  25897  usgruspgrb  26121  uspgrloopvtxel  26468  umgr2v2evtxel  26474  clwwlknonex2lem2  27083  3spthd  27154  grpoass  27485  lnolin  27737  elnlfn  28915  strlem4  29241  hstrlem4  29249  atmd  29386  nn0min  29695  omndadd  29834  slmdlema  29884  esumcvg  30276  measxun2  30401  sibfima  30528  bnj110  31054  bnj594  31108  bnj1491  31251  cvmcov  31371  mrsubcn  31542  dfon2lem5  31816  sssslt1  32031  madeval2  32061  ifscgr  32276  nn0prpw  32443  neibastop2lem  32480  bj-restb  33172  poimirlem25  33564  poimirlem32  33571  mbfresfi  33586  totbndss  33706  ghomlinOLD  33817  rngodi  33833  rngodir  33834  rngoass  33835  rngohomadd  33898  rngohommul  33899  crngocom  33930  idladdcl  33948  idllmulcl  33949  idlrmulcl  33950  exlimddvf  34056  oposlem  34787  cvlexch1  34933  hlsuprexch  34985  lautle  35688  elrfirn2  37576  wepwsolem  37929  kelac1  37950  islssfg2  37958  lnmlssfg  37967  2elfz3nn0  41651  2elfz2melfz  41653  icceuelpartlem  41696  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017  bgoldbtbnd  42022  setrec2fun  42764
  Copyright terms: Public domain W3C validator