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  3538  vtocl3gf  3539  vtocl2g  3540  vtocl3g  3541  vtoclegftOLD  3555  sbcthdv  3769  elinsn  4674  axprlem4OLD  5384  swopolem  5556  wereu  5634  funssres  6560  dffv2  6956  fmptcof  7102  fnprb  7182  fntpb  7183  fliftfuns  7289  isorel  7301  oveqrspc2v  7414  caovclg  7581  caovcomg  7584  caovassg  7587  caovcang  7590  caovordig  7594  caovordg  7596  caovdig  7603  caovdirg  7606  caofidlcan  7691  peano5  7869  dmfexALT  7884  frpoins3xp3g  8120  fvmpocurryd  8250  qliftfuns  8777  nneneq  9170  ttrcltr  9669  ttrclselem2  9679  frins3  9708  cfslb  10219  hsmexlem4  10382  axdc3lem2  10404  axdc4lem  10408  adderpq  10909  mulerpq  10910  ltordlem  11703  lble  12135  uz11  12818  xrsupsslem  13267  xrinfmsslem  13268  xrsupss  13269  xrinfmss  13270  fseqsupubi  13943  hashbclem  14417  ccatass  14553  swrdswrd  14670  swrdccatin1  14690  swrdccatin2  14694  cshwcsh2id  14794  wwlktovf  14922  isercolllem1  15631  caucvgb  15646  zsum  15684  fsum  15686  fsumf1o  15689  fsumcvg2  15693  isummulc2  15728  fsum2dlem  15736  fsumcom2  15740  fsumshftm  15747  fsum0diag2  15749  fsum00  15764  fsumrlim  15777  o1fsum  15779  isumshft  15805  clim2prod  15854  ntrivcvgfvn0  15865  zprod  15903  fprod  15907  fprodf1o  15912  prodss  15913  fprodser  15915  fprodcllemf  15924  fprodm1s  15936  fprodp1s  15937  fprodabs  15940  fprod2dlem  15946  fprodcom2  15950  fprodefsum  16061  mod2eq1n2dvds  16317  sumeven  16357  lcmfun  16615  pythagtriplem4  16790  pcmptdvds  16865  prslem  18258  posi  18278  dlatmjdi  18482  lidrididd  18597  grpidinv2  18929  ghmlin  19153  cntzmhm2  19274  dprdss  19961  dprd2d2  19976  srgrz  20116  srglz  20117  ringinvnz1ne0  20209  rrgeq0i  20608  lmodlema  20771  islmodd  20772  lsscl  20848  lsslss  20867  lspdisjb  21036  lsslinds  21740  assalem  21766  fvmptnn04if  22736  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  ssnei2  23003  t1ficld  23214  t1sep2  23256  unconn  23316  1stcclb  23331  ptbasfi  23468  tx1stc  23537  qtoptop2  23586  r0sep  23635  ustincl  24095  ustdiag  24096  ustinvel  24097  ustexhalf  24098  psmet0  24196  psmettri2  24197  prdsdsf  24255  prdsxmet  24257  cncfi  24787  ovolfiniun  25402  mbfimaopnlem  25556  limciun  25795  dvcn  25823  dvmptfsum  25879  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  dvfsumlem3  25935  itgsubst  25956  fsumvma  27124  dchrelbasd  27150  dchrisumlem3  27402  sssslt1  27707  sssslt2  27708  madeval2  27761  elmade  27779  axcontlem9  28899  usgruspgrb  29110  uspgrloopvtxel  29444  umgr2v2evtxel  29450  clwwlknonex2lem2  30037  3spthd  30105  grpoass  30432  lnolin  30683  elnlfn  31857  strlem4  32183  hstrlem4  32191  atmd  32328  nn0min  32745  omndadd  33020  slmdlema  33156  qsxpid  33333  esumcvg  34076  measxun2  34200  sibfima  34329  bnj110  34848  bnj594  34902  bnj1491  35047  loop1cycl  35124  cvmcov  35250  mrsubcn  35506  dfon2lem5  35775  ifscgr  36032  nn0prpw  36311  neibastop2lem  36348  bj-restb  37082  poimirlem25  37639  poimirlem32  37646  mbfresfi  37660  totbndss  37771  ghomlinOLD  37882  rngodi  37898  rngodir  37899  rngoass  37900  rngohomadd  37963  rngohommul  37964  crngocom  37995  idladdcl  38013  idllmulcl  38014  idlrmulcl  38015  exlimddvf  38115  oposlem  39175  cvlexch1  39321  hlsuprexch  39375  lautle  40078  elrfirn2  42684  wepwsolem  43031  kelac1  43052  islssfg2  43060  lnmlssfg  43069  onov0suclim  43263  relprel  44941  ovolval5lem3  46652  2elfz3nn0  47317  2elfz2melfz  47319  icceuelpartlem  47436  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  bgoldbtbnd  47810  gpgedg2iv  48058  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem6  48114  oppcendc  49007  setrec2fun  49681