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  3513  vtocl3gf  3514  vtocl2g  3515  vtocl3g  3516  vtoclegft  3527  sbcthdv  3737  elinsn  4650  axprlem4  5358  swopolem  5524  wereu  5596  funssres  6507  dffv2  6895  fmptcof  7034  fnprb  7116  fntpb  7117  fliftfuns  7217  isorel  7229  oveqrspc2v  7334  caovclg  7496  caovcomg  7499  caovassg  7502  caovcang  7505  caovordig  7509  caovordg  7511  caovdig  7518  caovdirg  7521  peano5  7772  peano5OLD  7773  dmfexALT  7789  fvmpocurryd  8118  qliftfuns  8624  nneneq  9030  nneneqOLD  9042  ttrcltr  9518  ttrclselem2  9528  frins3  9557  cfslb  10068  hsmexlem4  10231  axdc3lem2  10253  axdc4lem  10257  adderpq  10758  mulerpq  10759  ltordlem  11546  lble  11973  uz11  12653  xrsupsslem  13087  xrinfmsslem  13088  xrsupss  13089  xrinfmss  13090  fseqsupubi  13744  hashbclem  14209  ccatass  14338  swrdswrd  14463  swrdccatin1  14483  swrdccatin2  14487  cshwcsh2id  14586  wwlktovf  14716  isercolllem1  15421  caucvgb  15436  zsum  15475  fsum  15477  fsumf1o  15480  fsumcvg2  15484  isummulc2  15519  fsum2dlem  15527  fsumcom2  15531  fsumshftm  15538  fsum0diag2  15540  fsum00  15555  fsumrlim  15568  o1fsum  15570  isumshft  15596  clim2prod  15645  ntrivcvgfvn0  15656  zprod  15692  fprod  15696  fprodf1o  15701  prodss  15702  fprodser  15704  fprodcllemf  15713  fprodm1s  15725  fprodp1s  15726  fprodabs  15729  fprod2dlem  15735  fprodcom2  15739  fprodefsum  15849  mod2eq1n2dvds  16101  sumeven  16141  lcmfun  16395  pythagtriplem4  16565  pcmptdvds  16640  prslem  18061  posi  18080  dlatmjdi  18286  lidrididd  18399  grpidinv2  18679  ghmlin  18884  cntzmhm2  18991  dprdss  19677  dprd2d2  19692  srgrz  19807  srglz  19808  ringinvnz1ne0  19876  lmodlema  20173  islmodd  20174  lsscl  20249  lsslss  20268  lspdisjb  20433  rrgeq0i  20605  lsslinds  21083  assalem  21109  fvmptnn04if  22043  chfacfscmulgsum  22054  chfacfpmmulgsum  22058  ssnei2  22312  t1ficld  22523  t1sep2  22565  unconn  22625  1stcclb  22640  ptbasfi  22777  tx1stc  22846  qtoptop2  22895  r0sep  22944  ustincl  23404  ustdiag  23405  ustinvel  23406  ustexhalf  23407  psmet0  23506  psmettri2  23507  prdsdsf  23565  prdsxmet  23567  cncfi  24102  ovolfiniun  24710  mbfimaopnlem  24864  limciun  25103  dvcn  25130  dvmptfsum  25184  dvfsumle  25230  dvfsumabs  25232  dvfsumlem3  25237  itgsubst  25258  fsumvma  26406  dchrelbasd  26432  dchrisumlem3  26684  axcontlem9  27385  usgruspgrb  27596  uspgrloopvtxel  27928  umgr2v2evtxel  27934  clwwlknonex2lem2  28517  3spthd  28585  grpoass  28910  lnolin  29161  elnlfn  30335  strlem4  30661  hstrlem4  30669  atmd  30806  nn0min  31179  omndadd  31377  slmdlema  31501  qsxpid  31603  esumcvg  32099  measxun2  32223  sibfima  32350  bnj110  32883  bnj594  32937  bnj1491  33082  loop1cycl  33144  cvmcov  33270  mrsubcn  33526  dfon2lem5  33808  frpoins3xp3g  33833  sssslt1  34034  sssslt2  34035  madeval2  34082  elmade  34096  ifscgr  34391  nn0prpw  34557  neibastop2lem  34594  bj-restb  35309  poimirlem25  35846  poimirlem32  35853  mbfresfi  35867  totbndss  35979  ghomlinOLD  36090  rngodi  36106  rngodir  36107  rngoass  36108  rngohomadd  36171  rngohommul  36172  crngocom  36203  idladdcl  36221  idllmulcl  36222  idlrmulcl  36223  exlimddvf  36323  oposlem  37238  cvlexch1  37384  hlsuprexch  37437  lautle  38140  elrfirn2  40555  wepwsolem  40905  kelac1  40926  islssfg2  40934  lnmlssfg  40943  ovolval5lem3  44242  2elfz3nn0  44866  2elfz2melfz  44868  icceuelpartlem  44945  wtgoldbnnsum4prm  45312  bgoldbnnsum3prm  45314  bgoldbtbnd  45319  setrec2fun  46456