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  579  vtocl2gf  3584  vtocl3gf  3585  vtocl2g  3586  vtocl3g  3587  vtoclegftOLD  3602  sbcthdv  3820  elinsn  4735  axprlem4  5444  swopolem  5618  wereu  5696  funssres  6622  dffv2  7017  fmptcof  7164  fnprb  7245  fntpb  7246  fliftfuns  7350  isorel  7362  oveqrspc2v  7475  caovclg  7642  caovcomg  7645  caovassg  7648  caovcang  7651  caovordig  7655  caovordg  7657  caovdig  7664  caovdirg  7667  peano5  7932  peano5OLD  7933  dmfexALT  7948  frpoins3xp3g  8182  fvmpocurryd  8312  qliftfuns  8862  nneneq  9272  nneneqOLD  9284  ttrcltr  9785  ttrclselem2  9795  frins3  9824  cfslb  10335  hsmexlem4  10498  axdc3lem2  10520  axdc4lem  10524  adderpq  11025  mulerpq  11026  ltordlem  11815  lble  12247  uz11  12928  xrsupsslem  13369  xrinfmsslem  13370  xrsupss  13371  xrinfmss  13372  fseqsupubi  14029  hashbclem  14501  ccatass  14636  swrdswrd  14753  swrdccatin1  14773  swrdccatin2  14777  cshwcsh2id  14877  wwlktovf  15005  isercolllem1  15713  caucvgb  15728  zsum  15766  fsum  15768  fsumf1o  15771  fsumcvg2  15775  isummulc2  15810  fsum2dlem  15818  fsumcom2  15822  fsumshftm  15829  fsum0diag2  15831  fsum00  15846  fsumrlim  15859  o1fsum  15861  isumshft  15887  clim2prod  15936  ntrivcvgfvn0  15947  zprod  15985  fprod  15989  fprodf1o  15994  prodss  15995  fprodser  15997  fprodcllemf  16006  fprodm1s  16018  fprodp1s  16019  fprodabs  16022  fprod2dlem  16028  fprodcom2  16032  fprodefsum  16143  mod2eq1n2dvds  16395  sumeven  16435  lcmfun  16692  pythagtriplem4  16866  pcmptdvds  16941  prslem  18368  posi  18387  dlatmjdi  18593  lidrididd  18708  grpidinv2  19037  ghmlin  19261  cntzmhm2  19382  dprdss  20073  dprd2d2  20088  srgrz  20234  srglz  20235  ringinvnz1ne0  20323  rrgeq0i  20721  lmodlema  20885  islmodd  20886  lsscl  20963  lsslss  20982  lspdisjb  21151  lsslinds  21874  assalem  21900  fvmptnn04if  22876  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  ssnei2  23145  t1ficld  23356  t1sep2  23398  unconn  23458  1stcclb  23473  ptbasfi  23610  tx1stc  23679  qtoptop2  23728  r0sep  23777  ustincl  24237  ustdiag  24238  ustinvel  24239  ustexhalf  24240  psmet0  24339  psmettri2  24340  prdsdsf  24398  prdsxmet  24400  cncfi  24939  ovolfiniun  25555  mbfimaopnlem  25709  limciun  25949  dvcn  25977  dvmptfsum  26033  dvfsumle  26080  dvfsumleOLD  26081  dvfsumabs  26083  dvfsumlem3  26089  itgsubst  26110  fsumvma  27275  dchrelbasd  27301  dchrisumlem3  27553  sssslt1  27858  sssslt2  27859  madeval2  27910  elmade  27924  axcontlem9  29005  usgruspgrb  29218  uspgrloopvtxel  29552  umgr2v2evtxel  29558  clwwlknonex2lem2  30140  3spthd  30208  grpoass  30535  lnolin  30786  elnlfn  31960  strlem4  32286  hstrlem4  32294  atmd  32431  nn0min  32824  omndadd  33056  slmdlema  33182  qsxpid  33355  esumcvg  34050  measxun2  34174  sibfima  34303  bnj110  34834  bnj594  34888  bnj1491  35033  loop1cycl  35105  cvmcov  35231  mrsubcn  35487  dfon2lem5  35751  ifscgr  36008  nn0prpw  36289  neibastop2lem  36326  bj-restb  37060  poimirlem25  37605  poimirlem32  37612  mbfresfi  37626  totbndss  37737  ghomlinOLD  37848  rngodi  37864  rngodir  37865  rngoass  37866  rngohomadd  37929  rngohommul  37930  crngocom  37961  idladdcl  37979  idllmulcl  37980  idlrmulcl  37981  exlimddvf  38081  oposlem  39138  cvlexch1  39284  hlsuprexch  39338  lautle  40041  elrfirn2  42652  wepwsolem  42999  kelac1  43020  islssfg2  43028  lnmlssfg  43037  onov0suclim  43236  ovolval5lem3  46575  2elfz3nn0  47231  2elfz2melfz  47233  icceuelpartlem  47309  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  bgoldbtbnd  47683  setrec2fun  48784