Theorem mpan9 507

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  sylan  580  vtocl2gf  3557  vtocl3gf  3558  vtocl2g  3559  vtocl3g  3560  vtoclegftOLD  3571  sbcthdv  3789  elinsn  4707  axprlem4  5417  swopolem  5591  wereu  5665  funssres  6581  dffv2  6972  fmptcof  7112  fnprb  7194  fntpb  7195  fliftfuns  7295  isorel  7307  oveqrspc2v  7420  caovclg  7582  caovcomg  7585  caovassg  7588  caovcang  7591  caovordig  7595  caovordg  7597  caovdig  7604  caovdirg  7607  peano5  7866  peano5OLD  7867  dmfexALT  7883  frpoins3xp3g  8109  fvmpocurryd  8238  qliftfuns  8781  nneneq  9192  nneneqOLD  9204  ttrcltr  9693  ttrclselem2  9703  frins3  9732  cfslb  10243  hsmexlem4  10406  axdc3lem2  10428  axdc4lem  10432  adderpq  10933  mulerpq  10934  ltordlem  11721  lble  12148  uz11  12829  xrsupsslem  13268  xrinfmsslem  13269  xrsupss  13270  xrinfmss  13271  fseqsupubi  13925  hashbclem  14393  ccatass  14520  swrdswrd  14637  swrdccatin1  14657  swrdccatin2  14661  cshwcsh2id  14761  wwlktovf  14889  isercolllem1  15593  caucvgb  15608  zsum  15646  fsum  15648  fsumf1o  15651  fsumcvg2  15655  isummulc2  15690  fsum2dlem  15698  fsumcom2  15702  fsumshftm  15709  fsum0diag2  15711  fsum00  15726  fsumrlim  15739  o1fsum  15741  isumshft  15767  clim2prod  15816  ntrivcvgfvn0  15827  zprod  15863  fprod  15867  fprodf1o  15872  prodss  15873  fprodser  15875  fprodcllemf  15884  fprodm1s  15896  fprodp1s  15897  fprodabs  15900  fprod2dlem  15906  fprodcom2  15910  fprodefsum  16020  mod2eq1n2dvds  16272  sumeven  16312  lcmfun  16564  pythagtriplem4  16734  pcmptdvds  16809  prslem  18233  posi  18252  dlatmjdi  18458  lidrididd  18571  grpidinv2  18856  ghmlin  19063  cntzmhm2  19170  dprdss  19858  dprd2d2  19873  srgrz  19988  srglz  19989  ringinvnz1ne0  20069  lmodlema  20425  islmodd  20426  lsscl  20502  lsslss  20521  lspdisjb  20688  rrgeq0i  20841  lsslinds  21319  assalem  21345  fvmptnn04if  22280  chfacfscmulgsum  22291  chfacfpmmulgsum  22295  ssnei2  22549  t1ficld  22760  t1sep2  22802  unconn  22862  1stcclb  22877  ptbasfi  23014  tx1stc  23083  qtoptop2  23132  r0sep  23181  ustincl  23641  ustdiag  23642  ustinvel  23643  ustexhalf  23644  psmet0  23743  psmettri2  23744  prdsdsf  23802  prdsxmet  23804  cncfi  24339  ovolfiniun  24947  mbfimaopnlem  25101  limciun  25340  dvcn  25367  dvmptfsum  25421  dvfsumle  25467  dvfsumabs  25469  dvfsumlem3  25474  itgsubst  25495  fsumvma  26643  dchrelbasd  26669  dchrisumlem3  26921  sssslt1  27222  sssslt2  27223  madeval2  27271  elmade  27285  axcontlem9  28095  usgruspgrb  28306  uspgrloopvtxel  28638  umgr2v2evtxel  28644  clwwlknonex2lem2  29226  3spthd  29294  grpoass  29619  lnolin  29870  elnlfn  31044  strlem4  31370  hstrlem4  31378  atmd  31515  nn0min  31897  omndadd  32095  slmdlema  32219  qsxpid  32336  esumcvg  32915  measxun2  33039  sibfima  33168  bnj110  33700  bnj594  33754  bnj1491  33899  loop1cycl  33959  cvmcov  34085  mrsubcn  34341  dfon2lem5  34589  ifscgr  34846  nn0prpw  35012  neibastop2lem  35049  bj-restb  35779  poimirlem25  36317  poimirlem32  36324  mbfresfi  36338  totbndss  36450  ghomlinOLD  36561  rngodi  36577  rngodir  36578  rngoass  36579  rngohomadd  36642  rngohommul  36643  crngocom  36674  idladdcl  36692  idllmulcl  36693  idlrmulcl  36694  exlimddvf  36794  oposlem  37857  cvlexch1  38003  hlsuprexch  38057  lautle  38760  elrfirn2  41205  wepwsolem  41555  kelac1  41576  islssfg2  41584  lnmlssfg  41593  onov0suclim  41795  ovolval5lem3  45143  2elfz3nn0  45796  2elfz2melfz  45798  icceuelpartlem  45875  wtgoldbnnsum4prm  46242  bgoldbnnsum3prm  46244  bgoldbtbnd  46249  setrec2fun  47385