Theorem mpan9 510

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  sylan  583  vtocl2gf  3518  vtocl3gf  3519  vtocl2g  3520  vtoclegft  3530  sbcthdv  3736  elinsn  4606  axprlem4  5292  swopolem  5447  wereu  5515  funssres  6368  dffv2  6733  fmptcof  6869  fnprb  6948  fntpb  6949  fliftfuns  7046  isorel  7058  oveqrspc2v  7162  caovclg  7320  caovcomg  7323  caovassg  7326  caovcang  7329  caovordig  7333  caovordg  7335  caovdig  7342  caovdirg  7345  peano5  7585  fvmpocurryd  7920  qliftfuns  8367  nneneq  8684  cfslb  9677  hsmexlem4  9840  axdc3lem2  9862  axdc4lem  9866  adderpq  10367  mulerpq  10368  ltordlem  11154  lble  11580  uz11  12255  xrsupsslem  12688  xrinfmsslem  12689  xrsupss  12690  xrinfmss  12691  fseqsupubi  13341  hashbclem  13806  ccatass  13933  swrdswrd  14058  swrdccatin1  14078  swrdccatin2  14082  cshwcsh2id  14181  wwlktovf  14311  isercolllem1  15013  caucvgb  15028  zsum  15067  fsum  15069  fsumf1o  15072  fsumcvg2  15076  isummulc2  15109  fsum2dlem  15117  fsumcom2  15121  fsumshftm  15128  fsum0diag2  15130  fsum00  15145  fsumrlim  15158  o1fsum  15160  isumshft  15186  clim2prod  15236  ntrivcvgfvn0  15247  zprod  15283  fprod  15287  fprodf1o  15292  prodss  15293  fprodser  15295  fprodcllemf  15304  fprodm1s  15316  fprodp1s  15317  fprodabs  15320  fprod2dlem  15326  fprodcom2  15330  fprodefsum  15440  mod2eq1n2dvds  15688  sumeven  15728  lcmfun  15979  pythagtriplem4  16146  pcmptdvds  16220  prslem  17533  posi  17552  dlatmjdi  17796  lidrididd  17872  grpidinv2  18150  ghmlin  18355  cntzmhm2  18462  dprdss  19144  dprd2d2  19159  srgrz  19269  srglz  19270  ringinvnz1ne0  19338  lmodlema  19632  islmodd  19633  lsscl  19707  lsslss  19726  lspdisjb  19891  rrgeq0i  20055  lsslinds  20520  assalem  20546  fvmptnn04if  21454  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  ssnei2  21721  t1ficld  21932  t1sep2  21974  unconn  22034  1stcclb  22049  ptbasfi  22186  tx1stc  22255  qtoptop2  22304  r0sep  22353  ustincl  22813  ustdiag  22814  ustinvel  22815  ustexhalf  22816  psmet0  22915  psmettri2  22916  prdsdsf  22974  prdsxmet  22976  cncfi  23499  ovolfiniun  24105  mbfimaopnlem  24259  limciun  24497  dvcn  24524  dvmptfsum  24578  dvfsumle  24624  dvfsumabs  24626  dvfsumlem3  24631  itgsubst  24652  fsumvma  25797  dchrelbasd  25823  dchrisumlem3  26075  axcontlem9  26766  usgruspgrb  26974  uspgrloopvtxel  27306  umgr2v2evtxel  27312  clwwlknonex2lem2  27893  3spthd  27961  grpoass  28286  lnolin  28537  elnlfn  29711  strlem4  30037  hstrlem4  30045  atmd  30182  nn0min  30562  omndadd  30757  slmdlema  30881  qsxpid  30978  esumcvg  31455  measxun2  31579  sibfima  31706  bnj110  32240  bnj594  32294  bnj1491  32439  loop1cycl  32497  cvmcov  32623  mrsubcn  32879  dfon2lem5  33145  sssslt1  33373  madeval2  33403  ifscgr  33618  nn0prpw  33784  neibastop2lem  33821  bj-restb  34509  poimirlem25  35082  poimirlem32  35089  mbfresfi  35103  totbndss  35215  ghomlinOLD  35326  rngodi  35342  rngodir  35343  rngoass  35344  rngohomadd  35407  rngohommul  35408  crngocom  35439  idladdcl  35457  idllmulcl  35458  idlrmulcl  35459  exlimddvf  35559  oposlem  36478  cvlexch1  36624  hlsuprexch  36677  lautle  37380  elrfirn2  39637  wepwsolem  39986  kelac1  40007  islssfg2  40015  lnmlssfg  40024  2elfz3nn0  43873  2elfz2melfz  43875  icceuelpartlem  43952  wtgoldbnnsum4prm  44320  bgoldbnnsum3prm  44322  bgoldbtbnd  44327  setrec2fun  45222