Theorem mpan9 505

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 406	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  sylan  578  vtocl2gf  3562  vtocl3gf  3563  vtocl2g  3564  vtocl3g  3565  vtoclegftOLD  3576  sbcthdv  3794  elinsn  4715  axprlem4  5425  swopolem  5599  wereu  5673  funssres  6593  dffv2  6987  fmptcof  7131  fnprb  7213  fntpb  7214  fliftfuns  7315  isorel  7327  oveqrspc2v  7440  caovclg  7603  caovcomg  7606  caovassg  7609  caovcang  7612  caovordig  7616  caovordg  7618  caovdig  7625  caovdirg  7628  peano5  7888  peano5OLD  7889  dmfexALT  7905  frpoins3xp3g  8131  fvmpocurryd  8260  qliftfuns  8802  nneneq  9213  nneneqOLD  9225  ttrcltr  9715  ttrclselem2  9725  frins3  9754  cfslb  10265  hsmexlem4  10428  axdc3lem2  10450  axdc4lem  10454  adderpq  10955  mulerpq  10956  ltordlem  11745  lble  12172  uz11  12853  xrsupsslem  13292  xrinfmsslem  13293  xrsupss  13294  xrinfmss  13295  fseqsupubi  13949  hashbclem  14417  ccatass  14544  swrdswrd  14661  swrdccatin1  14681  swrdccatin2  14685  cshwcsh2id  14785  wwlktovf  14913  isercolllem1  15617  caucvgb  15632  zsum  15670  fsum  15672  fsumf1o  15675  fsumcvg2  15679  isummulc2  15714  fsum2dlem  15722  fsumcom2  15726  fsumshftm  15733  fsum0diag2  15735  fsum00  15750  fsumrlim  15763  o1fsum  15765  isumshft  15791  clim2prod  15840  ntrivcvgfvn0  15851  zprod  15887  fprod  15891  fprodf1o  15896  prodss  15897  fprodser  15899  fprodcllemf  15908  fprodm1s  15920  fprodp1s  15921  fprodabs  15924  fprod2dlem  15930  fprodcom2  15934  fprodefsum  16044  mod2eq1n2dvds  16296  sumeven  16336  lcmfun  16588  pythagtriplem4  16758  pcmptdvds  16833  prslem  18257  posi  18276  dlatmjdi  18482  lidrididd  18597  grpidinv2  18920  ghmlin  19137  cntzmhm2  19249  dprdss  19942  dprd2d2  19957  srgrz  20103  srglz  20104  ringinvnz1ne0  20190  lmodlema  20621  islmodd  20622  lsscl  20699  lsslss  20718  lspdisjb  20886  rrgeq0i  21107  lsslinds  21607  assalem  21633  fvmptnn04if  22573  chfacfscmulgsum  22584  chfacfpmmulgsum  22588  ssnei2  22842  t1ficld  23053  t1sep2  23095  unconn  23155  1stcclb  23170  ptbasfi  23307  tx1stc  23376  qtoptop2  23425  r0sep  23474  ustincl  23934  ustdiag  23935  ustinvel  23936  ustexhalf  23937  psmet0  24036  psmettri2  24037  prdsdsf  24095  prdsxmet  24097  cncfi  24636  ovolfiniun  25252  mbfimaopnlem  25406  limciun  25645  dvcn  25672  dvmptfsum  25726  dvfsumle  25772  dvfsumabs  25774  dvfsumlem3  25779  itgsubst  25800  fsumvma  26950  dchrelbasd  26976  dchrisumlem3  27228  sssslt1  27531  sssslt2  27532  madeval2  27583  elmade  27597  axcontlem9  28495  usgruspgrb  28706  uspgrloopvtxel  29038  umgr2v2evtxel  29044  clwwlknonex2lem2  29626  3spthd  29694  grpoass  30021  lnolin  30272  elnlfn  31446  strlem4  31772  hstrlem4  31780  atmd  31917  nn0min  32291  omndadd  32492  slmdlema  32616  qsxpid  32746  esumcvg  33380  measxun2  33504  sibfima  33633  bnj110  34165  bnj594  34219  bnj1491  34364  loop1cycl  34424  cvmcov  34550  mrsubcn  34806  dfon2lem5  35061  ifscgr  35318  gg-dvfsumle  35470  nn0prpw  35513  neibastop2lem  35550  bj-restb  36280  poimirlem25  36818  poimirlem32  36825  mbfresfi  36839  totbndss  36950  ghomlinOLD  37061  rngodi  37077  rngodir  37078  rngoass  37079  rngohomadd  37142  rngohommul  37143  crngocom  37174  idladdcl  37192  idllmulcl  37193  idlrmulcl  37194  exlimddvf  37294  oposlem  38357  cvlexch1  38503  hlsuprexch  38557  lautle  39260  elrfirn2  41738  wepwsolem  42088  kelac1  42109  islssfg2  42117  lnmlssfg  42126  onov0suclim  42328  ovolval5lem3  45670  2elfz3nn0  46324  2elfz2melfz  46326  icceuelpartlem  46403  wtgoldbnnsum4prm  46770  bgoldbnnsum3prm  46772  bgoldbtbnd  46777  setrec2fun  47826