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  3527  vtocl3gf  3528  vtocl2g  3529  vtocl3g  3530  sbcthdv  3756  elinsn  4667  axprlem4OLD  5374  swopolem  5542  wereu  5620  funssres  6536  dffv2  6929  fmptcof  7075  fnprb  7154  fntpb  7155  fliftfuns  7260  isorel  7272  oveqrspc2v  7385  caovclg  7550  caovcomg  7553  caovassg  7556  caovcang  7559  caovordig  7563  caovordg  7565  caovdig  7572  caovdirg  7575  caofidlcan  7660  peano5  7835  dmfexALT  7850  frpoins3xp3g  8083  fvmpocurryd  8213  qliftfuns  8741  nneneq  9130  ttrcltr  9625  ttrclselem2  9635  frins3  9667  cfslb  10176  hsmexlem4  10339  axdc3lem2  10361  axdc4lem  10365  adderpq  10867  mulerpq  10868  ltordlem  11662  lble  12094  uz11  12776  xrsupsslem  13222  xrinfmsslem  13223  xrsupss  13224  xrinfmss  13225  fseqsupubi  13901  hashbclem  14375  ccatass  14512  swrdswrd  14628  swrdccatin1  14648  swrdccatin2  14652  cshwcsh2id  14751  wwlktovf  14879  isercolllem1  15588  caucvgb  15603  zsum  15641  fsum  15643  fsumf1o  15646  fsumcvg2  15650  isummulc2  15685  fsum2dlem  15693  fsumcom2  15697  fsumshftm  15704  fsum0diag2  15706  fsum00  15721  fsumrlim  15734  o1fsum  15736  isumshft  15762  clim2prod  15811  ntrivcvgfvn0  15822  zprod  15860  fprod  15864  fprodf1o  15869  prodss  15870  fprodser  15872  fprodcllemf  15881  fprodm1s  15893  fprodp1s  15894  fprodabs  15897  fprod2dlem  15903  fprodcom2  15907  fprodefsum  16018  mod2eq1n2dvds  16274  sumeven  16314  lcmfun  16572  pythagtriplem4  16747  pcmptdvds  16822  prslem  18220  posi  18240  dlatmjdi  18446  lidrididd  18595  grpidinv2  18927  ghmlin  19150  cntzmhm2  19271  dprdss  19960  dprd2d2  19975  omndadd  20057  srgrz  20142  srglz  20143  ringinvnz1ne0  20235  rrgeq0i  20632  lmodlema  20816  islmodd  20817  lsscl  20893  lsslss  20912  lspdisjb  21081  lsslinds  21786  assalem  21812  fvmptnn04if  22793  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  ssnei2  23060  t1ficld  23271  t1sep2  23313  unconn  23373  1stcclb  23388  ptbasfi  23525  tx1stc  23594  qtoptop2  23643  r0sep  23692  ustincl  24152  ustdiag  24153  ustinvel  24154  ustexhalf  24155  psmet0  24252  psmettri2  24253  prdsdsf  24311  prdsxmet  24313  cncfi  24843  ovolfiniun  25458  mbfimaopnlem  25612  limciun  25851  dvcn  25879  dvmptfsum  25935  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dvfsumlem3  25991  itgsubst  26012  fsumvma  27180  dchrelbasd  27206  dchrisumlem3  27458  ssslts1  27769  ssslts2  27770  madeval2  27829  elmade  27853  axcontlem9  29045  usgruspgrb  29256  uspgrloopvtxel  29590  umgr2v2evtxel  29596  clwwlknonex2lem2  30183  3spthd  30251  grpoass  30578  lnolin  30829  elnlfn  32003  strlem4  32329  hstrlem4  32337  atmd  32474  nn0min  32901  slmdlema  33285  qsxpid  33443  esumcvg  34243  measxun2  34367  sibfima  34495  bnj110  35014  bnj594  35068  bnj1491  35213  loop1cycl  35331  cvmcov  35457  mrsubcn  35713  dfon2lem5  35979  ifscgr  36238  nn0prpw  36517  neibastop2lem  36554  bj-restb  37299  poimirlem25  37846  poimirlem32  37853  mbfresfi  37867  totbndss  37978  ghomlinOLD  38089  rngodi  38105  rngodir  38106  rngoass  38107  rngohomadd  38170  rngohommul  38171  crngocom  38202  idladdcl  38220  idllmulcl  38221  idlrmulcl  38222  exlimddvf  38322  oposlem  39442  cvlexch1  39588  hlsuprexch  39641  lautle  40344  elrfirn2  42938  wepwsolem  43284  kelac1  43305  islssfg2  43313  lnmlssfg  43322  onov0suclim  43516  relprel  45192  ovolval5lem3  46898  2elfz3nn0  47562  2elfz2melfz  47564  icceuelpartlem  47681  wtgoldbnnsum4prm  48048  bgoldbnnsum3prm  48050  bgoldbtbnd  48055  gpgedg2iv  48313  pgnbgreunbgrlem3  48364  pgnbgreunbgrlem6  48370  oppcendc  49263  setrec2fun  49937