Theorem mpan9 508

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

Step	Hyp	Ref	Expression
1		mpan9.1	. . 3 ⊢ (𝜑 → 𝜓)
2		mpan9.2	. . 3 ⊢ (𝜒 → (𝜓 → 𝜃))
3	1, 2	syl5 34	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	impcom 409	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  sylan  581  vtocl2gf  3561  vtocl3gf  3562  vtocl2g  3563  vtocl3g  3564  vtoclegftOLD  3575  sbcthdv  3794  elinsn  4715  axprlem4  5425  swopolem  5599  wereu  5673  funssres  6593  dffv2  6987  fmptcof  7128  fnprb  7210  fntpb  7211  fliftfuns  7311  isorel  7323  oveqrspc2v  7436  caovclg  7599  caovcomg  7602  caovassg  7605  caovcang  7608  caovordig  7612  caovordg  7614  caovdig  7621  caovdirg  7624  peano5  7884  peano5OLD  7885  dmfexALT  7901  frpoins3xp3g  8127  fvmpocurryd  8256  qliftfuns  8798  nneneq  9209  nneneqOLD  9221  ttrcltr  9711  ttrclselem2  9721  frins3  9750  cfslb  10261  hsmexlem4  10424  axdc3lem2  10446  axdc4lem  10450  adderpq  10951  mulerpq  10952  ltordlem  11739  lble  12166  uz11  12847  xrsupsslem  13286  xrinfmsslem  13287  xrsupss  13288  xrinfmss  13289  fseqsupubi  13943  hashbclem  14411  ccatass  14538  swrdswrd  14655  swrdccatin1  14675  swrdccatin2  14679  cshwcsh2id  14779  wwlktovf  14907  isercolllem1  15611  caucvgb  15626  zsum  15664  fsum  15666  fsumf1o  15669  fsumcvg2  15673  isummulc2  15708  fsum2dlem  15716  fsumcom2  15720  fsumshftm  15727  fsum0diag2  15729  fsum00  15744  fsumrlim  15757  o1fsum  15759  isumshft  15785  clim2prod  15834  ntrivcvgfvn0  15845  zprod  15881  fprod  15885  fprodf1o  15890  prodss  15891  fprodser  15893  fprodcllemf  15902  fprodm1s  15914  fprodp1s  15915  fprodabs  15918  fprod2dlem  15924  fprodcom2  15928  fprodefsum  16038  mod2eq1n2dvds  16290  sumeven  16330  lcmfun  16582  pythagtriplem4  16752  pcmptdvds  16827  prslem  18251  posi  18270  dlatmjdi  18476  lidrididd  18589  grpidinv2  18882  ghmlin  19097  cntzmhm2  19206  dprdss  19899  dprd2d2  19914  srgrz  20030  srglz  20031  ringinvnz1ne0  20112  lmodlema  20476  islmodd  20477  lsscl  20553  lsslss  20572  lspdisjb  20739  rrgeq0i  20905  lsslinds  21386  assalem  21412  fvmptnn04if  22351  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  ssnei2  22620  t1ficld  22831  t1sep2  22873  unconn  22933  1stcclb  22948  ptbasfi  23085  tx1stc  23154  qtoptop2  23203  r0sep  23252  ustincl  23712  ustdiag  23713  ustinvel  23714  ustexhalf  23715  psmet0  23814  psmettri2  23815  prdsdsf  23873  prdsxmet  23875  cncfi  24410  ovolfiniun  25018  mbfimaopnlem  25172  limciun  25411  dvcn  25438  dvmptfsum  25492  dvfsumle  25538  dvfsumabs  25540  dvfsumlem3  25545  itgsubst  25566  fsumvma  26716  dchrelbasd  26742  dchrisumlem3  26994  sssslt1  27296  sssslt2  27297  madeval2  27348  elmade  27362  axcontlem9  28230  usgruspgrb  28441  uspgrloopvtxel  28773  umgr2v2evtxel  28779  clwwlknonex2lem2  29361  3spthd  29429  grpoass  29756  lnolin  30007  elnlfn  31181  strlem4  31507  hstrlem4  31515  atmd  31652  nn0min  32026  omndadd  32224  slmdlema  32348  qsxpid  32474  esumcvg  33084  measxun2  33208  sibfima  33337  bnj110  33869  bnj594  33923  bnj1491  34068  loop1cycl  34128  cvmcov  34254  mrsubcn  34510  dfon2lem5  34759  ifscgr  35016  gg-dvfsumle  35182  nn0prpw  35208  neibastop2lem  35245  bj-restb  35975  poimirlem25  36513  poimirlem32  36520  mbfresfi  36534  totbndss  36645  ghomlinOLD  36756  rngodi  36772  rngodir  36773  rngoass  36774  rngohomadd  36837  rngohommul  36838  crngocom  36869  idladdcl  36887  idllmulcl  36888  idlrmulcl  36889  exlimddvf  36989  oposlem  38052  cvlexch1  38198  hlsuprexch  38252  lautle  38955  elrfirn2  41434  wepwsolem  41784  kelac1  41805  islssfg2  41813  lnmlssfg  41822  onov0suclim  42024  ovolval5lem3  45370  2elfz3nn0  46024  2elfz2melfz  46026  icceuelpartlem  46103  wtgoldbnnsum4prm  46470  bgoldbnnsum3prm  46472  bgoldbtbnd  46477  setrec2fun  47737