Theorem mpan9 509

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  sylan  582  vtocl2gf  3570  vtocl3gf  3571  vtocl2g  3572  vtoclegft  3582  sbcthdv  3788  elinsn  4646  axprlem4  5327  swopolem  5483  wereu  5551  funssres  6398  dffv2  6756  fmptcof  6892  fnprb  6971  fntpb  6972  fliftfuns  7067  isorel  7079  oveqrspc2v  7183  caovclg  7340  caovcomg  7343  caovassg  7346  caovcang  7349  caovordig  7353  caovordg  7355  caovdig  7362  caovdirg  7365  peano5  7605  fvmpocurryd  7937  qliftfuns  8384  nneneq  8700  cfslb  9688  hsmexlem4  9851  axdc3lem2  9873  axdc4lem  9877  adderpq  10378  mulerpq  10379  ltordlem  11165  lble  11593  uz11  12268  xrsupsslem  12701  xrinfmsslem  12702  xrsupss  12703  xrinfmss  12704  fseqsupubi  13347  hashbclem  13811  ccatass  13942  swrdswrd  14067  swrdccatin1  14087  swrdccatin2  14091  cshwcsh2id  14190  wwlktovf  14320  isercolllem1  15021  caucvgb  15036  zsum  15075  fsum  15077  fsumf1o  15080  fsumcvg2  15084  isummulc2  15117  fsum2dlem  15125  fsumcom2  15129  fsumshftm  15136  fsum0diag2  15138  fsum00  15153  fsumrlim  15166  o1fsum  15168  isumshft  15194  clim2prod  15244  ntrivcvgfvn0  15255  zprod  15291  fprod  15295  fprodf1o  15300  prodss  15301  fprodser  15303  fprodcllemf  15312  fprodm1s  15324  fprodp1s  15325  fprodabs  15328  fprod2dlem  15334  fprodcom2  15338  fprodefsum  15448  mod2eq1n2dvds  15696  sumeven  15738  lcmfun  15989  pythagtriplem4  16156  pcmptdvds  16230  prslem  17541  posi  17560  dlatmjdi  17804  lidrididd  17880  grpidinv2  18158  ghmlin  18363  cntzmhm2  18470  dprdss  19151  dprd2d2  19166  srgrz  19276  srglz  19277  ringinvnz1ne0  19342  lmodlema  19639  islmodd  19640  lsscl  19714  lsslss  19733  lspdisjb  19898  rrgeq0i  20062  assalem  20089  lsslinds  20975  fvmptnn04if  21457  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  ssnei2  21724  t1ficld  21935  t1sep2  21977  unconn  22037  1stcclb  22052  ptbasfi  22189  tx1stc  22258  qtoptop2  22307  r0sep  22356  ustincl  22816  ustdiag  22817  ustinvel  22818  ustexhalf  22819  psmet0  22918  psmettri2  22919  prdsdsf  22977  prdsxmet  22979  cncfi  23502  ovolfiniun  24102  mbfimaopnlem  24256  limciun  24492  dvcn  24518  dvmptfsum  24572  dvfsumle  24618  dvfsumabs  24620  dvfsumlem3  24625  itgsubst  24646  fsumvma  25789  dchrelbasd  25815  dchrisumlem3  26067  axcontlem9  26758  usgruspgrb  26966  uspgrloopvtxel  27298  umgr2v2evtxel  27304  clwwlknonex2lem2  27887  3spthd  27955  grpoass  28280  lnolin  28531  elnlfn  29705  strlem4  30031  hstrlem4  30039  atmd  30176  nn0min  30536  omndadd  30707  slmdlema  30831  qsxpid  30927  esumcvg  31345  measxun2  31469  sibfima  31596  bnj110  32130  bnj594  32184  bnj1491  32329  loop1cycl  32384  cvmcov  32510  mrsubcn  32766  dfon2lem5  33032  sssslt1  33260  madeval2  33290  ifscgr  33505  nn0prpw  33671  neibastop2lem  33708  bj-restb  34388  poimirlem25  34932  poimirlem32  34939  mbfresfi  34953  totbndss  35070  ghomlinOLD  35181  rngodi  35197  rngodir  35198  rngoass  35199  rngohomadd  35262  rngohommul  35263  crngocom  35294  idladdcl  35312  idllmulcl  35313  idlrmulcl  35314  exlimddvf  35414  oposlem  36333  cvlexch1  36479  hlsuprexch  36532  lautle  37235  elrfirn2  39313  wepwsolem  39662  kelac1  39683  islssfg2  39691  lnmlssfg  39700  2elfz3nn0  43536  2elfz2melfz  43538  icceuelpartlem  43615  wtgoldbnnsum4prm  43987  bgoldbnnsum3prm  43989  bgoldbtbnd  43994  setrec2fun  44815