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 206  df-an 396

This theorem is referenced by:  sylan  579  vtocl2gf  3506  vtocl3gf  3507  vtocl2g  3508  vtocl3g  3509  vtoclegft  3520  sbcthdv  3735  elinsn  4651  axprlem4  5352  swopolem  5512  wereu  5584  funssres  6474  dffv2  6857  fmptcof  6996  fnprb  7078  fntpb  7079  fliftfuns  7178  isorel  7190  oveqrspc2v  7295  caovclg  7455  caovcomg  7458  caovassg  7461  caovcang  7464  caovordig  7468  caovordg  7470  caovdig  7477  caovdirg  7480  peano5  7727  peano5OLD  7728  dmfexALT  7744  fvmpocurryd  8071  qliftfuns  8567  nneneq  8956  nneneqOLD  8969  ttrcltr  9435  ttrclselem2  9445  frins3  9497  cfslb  10006  hsmexlem4  10169  axdc3lem2  10191  axdc4lem  10195  adderpq  10696  mulerpq  10697  ltordlem  11483  lble  11910  uz11  12589  xrsupsslem  13023  xrinfmsslem  13024  xrsupss  13025  xrinfmss  13026  fseqsupubi  13679  hashbclem  14145  ccatass  14274  swrdswrd  14399  swrdccatin1  14419  swrdccatin2  14423  cshwcsh2id  14522  wwlktovf  14652  isercolllem1  15357  caucvgb  15372  zsum  15411  fsum  15413  fsumf1o  15416  fsumcvg2  15420  isummulc2  15455  fsum2dlem  15463  fsumcom2  15467  fsumshftm  15474  fsum0diag2  15476  fsum00  15491  fsumrlim  15504  o1fsum  15506  isumshft  15532  clim2prod  15581  ntrivcvgfvn0  15592  zprod  15628  fprod  15632  fprodf1o  15637  prodss  15638  fprodser  15640  fprodcllemf  15649  fprodm1s  15661  fprodp1s  15662  fprodabs  15665  fprod2dlem  15671  fprodcom2  15675  fprodefsum  15785  mod2eq1n2dvds  16037  sumeven  16077  lcmfun  16331  pythagtriplem4  16501  pcmptdvds  16576  prslem  17997  posi  18016  dlatmjdi  18222  lidrididd  18335  grpidinv2  18615  ghmlin  18820  cntzmhm2  18927  dprdss  19613  dprd2d2  19628  srgrz  19743  srglz  19744  ringinvnz1ne0  19812  lmodlema  20109  islmodd  20110  lsscl  20185  lsslss  20204  lspdisjb  20369  rrgeq0i  20541  lsslinds  21019  assalem  21045  fvmptnn04if  21979  chfacfscmulgsum  21990  chfacfpmmulgsum  21994  ssnei2  22248  t1ficld  22459  t1sep2  22501  unconn  22561  1stcclb  22576  ptbasfi  22713  tx1stc  22782  qtoptop2  22831  r0sep  22880  ustincl  23340  ustdiag  23341  ustinvel  23342  ustexhalf  23343  psmet0  23442  psmettri2  23443  prdsdsf  23501  prdsxmet  23503  cncfi  24038  ovolfiniun  24646  mbfimaopnlem  24800  limciun  25039  dvcn  25066  dvmptfsum  25120  dvfsumle  25166  dvfsumabs  25168  dvfsumlem3  25173  itgsubst  25194  fsumvma  26342  dchrelbasd  26368  dchrisumlem3  26620  axcontlem9  27321  usgruspgrb  27532  uspgrloopvtxel  27864  umgr2v2evtxel  27870  clwwlknonex2lem2  28451  3spthd  28519  grpoass  28844  lnolin  29095  elnlfn  30269  strlem4  30595  hstrlem4  30603  atmd  30740  nn0min  31113  omndadd  31311  slmdlema  31435  qsxpid  31537  esumcvg  32033  measxun2  32157  sibfima  32284  bnj110  32817  bnj594  32871  bnj1491  33016  loop1cycl  33078  cvmcov  33204  mrsubcn  33460  dfon2lem5  33742  frpoins3xp3g  33767  sssslt1  33968  sssslt2  33969  madeval2  34016  elmade  34030  ifscgr  34325  nn0prpw  34491  neibastop2lem  34528  bj-restb  35244  poimirlem25  35781  poimirlem32  35788  mbfresfi  35802  totbndss  35914  ghomlinOLD  36025  rngodi  36041  rngodir  36042  rngoass  36043  rngohomadd  36106  rngohommul  36107  crngocom  36138  idladdcl  36156  idllmulcl  36157  idlrmulcl  36158  exlimddvf  36258  oposlem  37175  cvlexch1  37321  hlsuprexch  37374  lautle  38077  elrfirn2  40498  wepwsolem  40847  kelac1  40868  islssfg2  40876  lnmlssfg  40885  2elfz3nn0  44760  2elfz2melfz  44762  icceuelpartlem  44839  wtgoldbnnsum4prm  45206  bgoldbnnsum3prm  45208  bgoldbtbnd  45213  setrec2fun  46350