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  3572  vtocl3gf  3573  vtocl2g  3574  vtocl3g  3575  vtoclegftOLD  3589  sbcthdv  3804  elinsn  4710  axprlem4OLD  5429  swopolem  5602  wereu  5681  funssres  6610  dffv2  7004  fmptcof  7150  fnprb  7228  fntpb  7229  fliftfuns  7334  isorel  7346  oveqrspc2v  7458  caovclg  7625  caovcomg  7628  caovassg  7631  caovcang  7634  caovordig  7638  caovordg  7640  caovdig  7647  caovdirg  7650  caofidlcan  7735  peano5  7915  dmfexALT  7930  frpoins3xp3g  8166  fvmpocurryd  8296  qliftfuns  8844  nneneq  9246  nneneqOLD  9258  ttrcltr  9756  ttrclselem2  9766  frins3  9795  cfslb  10306  hsmexlem4  10469  axdc3lem2  10491  axdc4lem  10495  adderpq  10996  mulerpq  10997  ltordlem  11788  lble  12220  uz11  12903  xrsupsslem  13349  xrinfmsslem  13350  xrsupss  13351  xrinfmss  13352  fseqsupubi  14019  hashbclem  14491  ccatass  14626  swrdswrd  14743  swrdccatin1  14763  swrdccatin2  14767  cshwcsh2id  14867  wwlktovf  14995  isercolllem1  15701  caucvgb  15716  zsum  15754  fsum  15756  fsumf1o  15759  fsumcvg2  15763  isummulc2  15798  fsum2dlem  15806  fsumcom2  15810  fsumshftm  15817  fsum0diag2  15819  fsum00  15834  fsumrlim  15847  o1fsum  15849  isumshft  15875  clim2prod  15924  ntrivcvgfvn0  15935  zprod  15973  fprod  15977  fprodf1o  15982  prodss  15983  fprodser  15985  fprodcllemf  15994  fprodm1s  16006  fprodp1s  16007  fprodabs  16010  fprod2dlem  16016  fprodcom2  16020  fprodefsum  16131  mod2eq1n2dvds  16384  sumeven  16424  lcmfun  16682  pythagtriplem4  16857  pcmptdvds  16932  prslem  18343  posi  18363  dlatmjdi  18568  lidrididd  18683  grpidinv2  19015  ghmlin  19239  cntzmhm2  19360  dprdss  20049  dprd2d2  20064  srgrz  20204  srglz  20205  ringinvnz1ne0  20297  rrgeq0i  20699  lmodlema  20863  islmodd  20864  lsscl  20940  lsslss  20959  lspdisjb  21128  lsslinds  21851  assalem  21877  fvmptnn04if  22855  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  ssnei2  23124  t1ficld  23335  t1sep2  23377  unconn  23437  1stcclb  23452  ptbasfi  23589  tx1stc  23658  qtoptop2  23707  r0sep  23756  ustincl  24216  ustdiag  24217  ustinvel  24218  ustexhalf  24219  psmet0  24318  psmettri2  24319  prdsdsf  24377  prdsxmet  24379  cncfi  24920  ovolfiniun  25536  mbfimaopnlem  25690  limciun  25929  dvcn  25957  dvmptfsum  26013  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  dvfsumlem3  26069  itgsubst  26090  fsumvma  27257  dchrelbasd  27283  dchrisumlem3  27535  sssslt1  27840  sssslt2  27841  madeval2  27892  elmade  27906  axcontlem9  28987  usgruspgrb  29200  uspgrloopvtxel  29534  umgr2v2evtxel  29540  clwwlknonex2lem2  30127  3spthd  30195  grpoass  30522  lnolin  30773  elnlfn  31947  strlem4  32273  hstrlem4  32281  atmd  32418  nn0min  32822  omndadd  33083  slmdlema  33209  qsxpid  33390  esumcvg  34087  measxun2  34211  sibfima  34340  bnj110  34872  bnj594  34926  bnj1491  35071  loop1cycl  35142  cvmcov  35268  mrsubcn  35524  dfon2lem5  35788  ifscgr  36045  nn0prpw  36324  neibastop2lem  36361  bj-restb  37095  poimirlem25  37652  poimirlem32  37659  mbfresfi  37673  totbndss  37784  ghomlinOLD  37895  rngodi  37911  rngodir  37912  rngoass  37913  rngohomadd  37976  rngohommul  37977  crngocom  38008  idladdcl  38026  idllmulcl  38027  idlrmulcl  38028  exlimddvf  38128  oposlem  39183  cvlexch1  39329  hlsuprexch  39383  lautle  40086  elrfirn2  42707  wepwsolem  43054  kelac1  43075  islssfg2  43083  lnmlssfg  43092  onov0suclim  43287  relprel  44972  ovolval5lem3  46669  2elfz3nn0  47328  2elfz2melfz  47330  icceuelpartlem  47422  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  bgoldbtbnd  47796  oppcendc  48906  setrec2fun  49211