Theorem mpan9 506

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  sylan  580  vtocl2gf  3571  vtocl3gf  3572  vtocl2g  3573  vtocl3g  3574  vtoclegftOLD  3588  sbcthdv  3806  elinsn  4714  axprlem4OLD  5434  swopolem  5606  wereu  5684  funssres  6611  dffv2  7003  fmptcof  7149  fnprb  7227  fntpb  7228  fliftfuns  7333  isorel  7345  oveqrspc2v  7457  caovclg  7624  caovcomg  7627  caovassg  7630  caovcang  7633  caovordig  7637  caovordg  7639  caovdig  7646  caovdirg  7649  peano5  7915  dmfexALT  7930  frpoins3xp3g  8164  fvmpocurryd  8294  qliftfuns  8842  nneneq  9243  nneneqOLD  9255  ttrcltr  9753  ttrclselem2  9763  frins3  9792  cfslb  10303  hsmexlem4  10466  axdc3lem2  10488  axdc4lem  10492  adderpq  10993  mulerpq  10994  ltordlem  11785  lble  12217  uz11  12900  xrsupsslem  13345  xrinfmsslem  13346  xrsupss  13347  xrinfmss  13348  fseqsupubi  14015  hashbclem  14487  ccatass  14622  swrdswrd  14739  swrdccatin1  14759  swrdccatin2  14763  cshwcsh2id  14863  wwlktovf  14991  isercolllem1  15697  caucvgb  15712  zsum  15750  fsum  15752  fsumf1o  15755  fsumcvg2  15759  isummulc2  15794  fsum2dlem  15802  fsumcom2  15806  fsumshftm  15813  fsum0diag2  15815  fsum00  15830  fsumrlim  15843  o1fsum  15845  isumshft  15871  clim2prod  15920  ntrivcvgfvn0  15931  zprod  15969  fprod  15973  fprodf1o  15978  prodss  15979  fprodser  15981  fprodcllemf  15990  fprodm1s  16002  fprodp1s  16003  fprodabs  16006  fprod2dlem  16012  fprodcom2  16016  fprodefsum  16127  mod2eq1n2dvds  16380  sumeven  16420  lcmfun  16678  pythagtriplem4  16852  pcmptdvds  16927  prslem  18354  posi  18374  dlatmjdi  18580  lidrididd  18695  grpidinv2  19027  ghmlin  19251  cntzmhm2  19372  dprdss  20063  dprd2d2  20078  srgrz  20224  srglz  20225  ringinvnz1ne0  20313  rrgeq0i  20715  lmodlema  20879  islmodd  20880  lsscl  20957  lsslss  20976  lspdisjb  21145  lsslinds  21868  assalem  21894  fvmptnn04if  22870  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  ssnei2  23139  t1ficld  23350  t1sep2  23392  unconn  23452  1stcclb  23467  ptbasfi  23604  tx1stc  23673  qtoptop2  23722  r0sep  23771  ustincl  24231  ustdiag  24232  ustinvel  24233  ustexhalf  24234  psmet0  24333  psmettri2  24334  prdsdsf  24392  prdsxmet  24394  cncfi  24933  ovolfiniun  25549  mbfimaopnlem  25703  limciun  25943  dvcn  25971  dvmptfsum  26027  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  dvfsumlem3  26083  itgsubst  26104  fsumvma  27271  dchrelbasd  27297  dchrisumlem3  27549  sssslt1  27854  sssslt2  27855  madeval2  27906  elmade  27920  axcontlem9  29001  usgruspgrb  29214  uspgrloopvtxel  29548  umgr2v2evtxel  29554  clwwlknonex2lem2  30136  3spthd  30204  grpoass  30531  lnolin  30782  elnlfn  31956  strlem4  32282  hstrlem4  32290  atmd  32427  nn0min  32826  omndadd  33065  slmdlema  33191  qsxpid  33369  esumcvg  34066  measxun2  34190  sibfima  34319  bnj110  34850  bnj594  34904  bnj1491  35049  loop1cycl  35121  cvmcov  35247  mrsubcn  35503  dfon2lem5  35768  ifscgr  36025  nn0prpw  36305  neibastop2lem  36342  bj-restb  37076  poimirlem25  37631  poimirlem32  37638  mbfresfi  37652  totbndss  37763  ghomlinOLD  37874  rngodi  37890  rngodir  37891  rngoass  37892  rngohomadd  37955  rngohommul  37956  crngocom  37987  idladdcl  38005  idllmulcl  38006  idlrmulcl  38007  exlimddvf  38107  oposlem  39163  cvlexch1  39309  hlsuprexch  39363  lautle  40066  elrfirn2  42683  wepwsolem  43030  kelac1  43051  islssfg2  43059  lnmlssfg  43068  onov0suclim  43263  ovolval5lem3  46609  2elfz3nn0  47265  2elfz2melfz  47267  icceuelpartlem  47359  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  bgoldbtbnd  47733  setrec2fun  48922