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  3535  vtocl3gf  3536  vtocl2g  3537  vtocl3g  3538  vtoclegftOLD  3552  sbcthdv  3766  elinsn  4670  axprlem4OLD  5379  swopolem  5549  wereu  5627  funssres  6544  dffv2  6938  fmptcof  7084  fnprb  7164  fntpb  7165  fliftfuns  7271  isorel  7283  oveqrspc2v  7396  caovclg  7561  caovcomg  7564  caovassg  7567  caovcang  7570  caovordig  7574  caovordg  7576  caovdig  7583  caovdirg  7586  caofidlcan  7671  peano5  7849  dmfexALT  7864  frpoins3xp3g  8097  fvmpocurryd  8227  qliftfuns  8754  nneneq  9147  ttrcltr  9645  ttrclselem2  9655  frins3  9684  cfslb  10195  hsmexlem4  10358  axdc3lem2  10380  axdc4lem  10384  adderpq  10885  mulerpq  10886  ltordlem  11679  lble  12111  uz11  12794  xrsupsslem  13243  xrinfmsslem  13244  xrsupss  13245  xrinfmss  13246  fseqsupubi  13919  hashbclem  14393  ccatass  14529  swrdswrd  14646  swrdccatin1  14666  swrdccatin2  14670  cshwcsh2id  14770  wwlktovf  14898  isercolllem1  15607  caucvgb  15622  zsum  15660  fsum  15662  fsumf1o  15665  fsumcvg2  15669  isummulc2  15704  fsum2dlem  15712  fsumcom2  15716  fsumshftm  15723  fsum0diag2  15725  fsum00  15740  fsumrlim  15753  o1fsum  15755  isumshft  15781  clim2prod  15830  ntrivcvgfvn0  15841  zprod  15879  fprod  15883  fprodf1o  15888  prodss  15889  fprodser  15891  fprodcllemf  15900  fprodm1s  15912  fprodp1s  15913  fprodabs  15916  fprod2dlem  15922  fprodcom2  15926  fprodefsum  16037  mod2eq1n2dvds  16293  sumeven  16333  lcmfun  16591  pythagtriplem4  16766  pcmptdvds  16841  prslem  18234  posi  18254  dlatmjdi  18458  lidrididd  18573  grpidinv2  18905  ghmlin  19129  cntzmhm2  19250  dprdss  19937  dprd2d2  19952  srgrz  20092  srglz  20093  ringinvnz1ne0  20185  rrgeq0i  20584  lmodlema  20747  islmodd  20748  lsscl  20824  lsslss  20843  lspdisjb  21012  lsslinds  21716  assalem  21742  fvmptnn04if  22712  chfacfscmulgsum  22723  chfacfpmmulgsum  22727  ssnei2  22979  t1ficld  23190  t1sep2  23232  unconn  23292  1stcclb  23307  ptbasfi  23444  tx1stc  23513  qtoptop2  23562  r0sep  23611  ustincl  24071  ustdiag  24072  ustinvel  24073  ustexhalf  24074  psmet0  24172  psmettri2  24173  prdsdsf  24231  prdsxmet  24233  cncfi  24763  ovolfiniun  25378  mbfimaopnlem  25532  limciun  25771  dvcn  25799  dvmptfsum  25855  dvfsumle  25902  dvfsumleOLD  25903  dvfsumabs  25905  dvfsumlem3  25911  itgsubst  25932  fsumvma  27100  dchrelbasd  27126  dchrisumlem3  27378  sssslt1  27683  sssslt2  27684  madeval2  27737  elmade  27755  axcontlem9  28875  usgruspgrb  29086  uspgrloopvtxel  29420  umgr2v2evtxel  29426  clwwlknonex2lem2  30010  3spthd  30078  grpoass  30405  lnolin  30656  elnlfn  31830  strlem4  32156  hstrlem4  32164  atmd  32301  nn0min  32718  omndadd  32993  slmdlema  33129  qsxpid  33306  esumcvg  34049  measxun2  34173  sibfima  34302  bnj110  34821  bnj594  34875  bnj1491  35020  loop1cycl  35097  cvmcov  35223  mrsubcn  35479  dfon2lem5  35748  ifscgr  36005  nn0prpw  36284  neibastop2lem  36321  bj-restb  37055  poimirlem25  37612  poimirlem32  37619  mbfresfi  37633  totbndss  37744  ghomlinOLD  37855  rngodi  37871  rngodir  37872  rngoass  37873  rngohomadd  37936  rngohommul  37937  crngocom  37968  idladdcl  37986  idllmulcl  37987  idlrmulcl  37988  exlimddvf  38088  oposlem  39148  cvlexch1  39294  hlsuprexch  39348  lautle  40051  elrfirn2  42657  wepwsolem  43004  kelac1  43025  islssfg2  43033  lnmlssfg  43042  onov0suclim  43236  relprel  44914  ovolval5lem3  46625  2elfz3nn0  47290  2elfz2melfz  47292  icceuelpartlem  47409  wtgoldbnnsum4prm  47776  bgoldbnnsum3prm  47778  bgoldbtbnd  47783  gpgedg2iv  48031  pgnbgreunbgrlem3  48081  pgnbgreunbgrlem6  48087  oppcendc  48980  setrec2fun  49654