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  3551  vtocl3gf  3552  vtocl2g  3553  vtocl3g  3554  vtoclegftOLD  3568  sbcthdv  3781  elinsn  4686  axprlem4OLD  5399  swopolem  5571  wereu  5650  funssres  6579  dffv2  6973  fmptcof  7119  fnprb  7199  fntpb  7200  fliftfuns  7306  isorel  7318  oveqrspc2v  7430  caovclg  7597  caovcomg  7600  caovassg  7603  caovcang  7606  caovordig  7610  caovordg  7612  caovdig  7619  caovdirg  7622  caofidlcan  7707  peano5  7887  dmfexALT  7902  frpoins3xp3g  8138  fvmpocurryd  8268  qliftfuns  8816  nneneq  9218  ttrcltr  9728  ttrclselem2  9738  frins3  9767  cfslb  10278  hsmexlem4  10441  axdc3lem2  10463  axdc4lem  10467  adderpq  10968  mulerpq  10969  ltordlem  11760  lble  12192  uz11  12875  xrsupsslem  13321  xrinfmsslem  13322  xrsupss  13323  xrinfmss  13324  fseqsupubi  13994  hashbclem  14468  ccatass  14604  swrdswrd  14721  swrdccatin1  14741  swrdccatin2  14745  cshwcsh2id  14845  wwlktovf  14973  isercolllem1  15679  caucvgb  15694  zsum  15732  fsum  15734  fsumf1o  15737  fsumcvg2  15741  isummulc2  15776  fsum2dlem  15784  fsumcom2  15788  fsumshftm  15795  fsum0diag2  15797  fsum00  15812  fsumrlim  15825  o1fsum  15827  isumshft  15853  clim2prod  15902  ntrivcvgfvn0  15913  zprod  15951  fprod  15955  fprodf1o  15960  prodss  15961  fprodser  15963  fprodcllemf  15972  fprodm1s  15984  fprodp1s  15985  fprodabs  15988  fprod2dlem  15994  fprodcom2  15998  fprodefsum  16109  mod2eq1n2dvds  16364  sumeven  16404  lcmfun  16662  pythagtriplem4  16837  pcmptdvds  16912  prslem  18307  posi  18327  dlatmjdi  18531  lidrididd  18646  grpidinv2  18978  ghmlin  19202  cntzmhm2  19323  dprdss  20010  dprd2d2  20025  srgrz  20165  srglz  20166  ringinvnz1ne0  20258  rrgeq0i  20657  lmodlema  20820  islmodd  20821  lsscl  20897  lsslss  20916  lspdisjb  21085  lsslinds  21789  assalem  21815  fvmptnn04if  22785  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  ssnei2  23052  t1ficld  23263  t1sep2  23305  unconn  23365  1stcclb  23380  ptbasfi  23517  tx1stc  23586  qtoptop2  23635  r0sep  23684  ustincl  24144  ustdiag  24145  ustinvel  24146  ustexhalf  24147  psmet0  24245  psmettri2  24246  prdsdsf  24304  prdsxmet  24306  cncfi  24836  ovolfiniun  25452  mbfimaopnlem  25606  limciun  25845  dvcn  25873  dvmptfsum  25929  dvfsumle  25976  dvfsumleOLD  25977  dvfsumabs  25979  dvfsumlem3  25985  itgsubst  26006  fsumvma  27174  dchrelbasd  27200  dchrisumlem3  27452  sssslt1  27757  sssslt2  27758  madeval2  27809  elmade  27823  axcontlem9  28897  usgruspgrb  29108  uspgrloopvtxel  29442  umgr2v2evtxel  29448  clwwlknonex2lem2  30035  3spthd  30103  grpoass  30430  lnolin  30681  elnlfn  31855  strlem4  32181  hstrlem4  32189  atmd  32326  nn0min  32745  omndadd  33020  slmdlema  33146  qsxpid  33323  esumcvg  34063  measxun2  34187  sibfima  34316  bnj110  34835  bnj594  34889  bnj1491  35034  loop1cycl  35105  cvmcov  35231  mrsubcn  35487  dfon2lem5  35751  ifscgr  36008  nn0prpw  36287  neibastop2lem  36324  bj-restb  37058  poimirlem25  37615  poimirlem32  37622  mbfresfi  37636  totbndss  37747  ghomlinOLD  37858  rngodi  37874  rngodir  37875  rngoass  37876  rngohomadd  37939  rngohommul  37940  crngocom  37971  idladdcl  37989  idllmulcl  37990  idlrmulcl  37991  exlimddvf  38091  oposlem  39146  cvlexch1  39292  hlsuprexch  39346  lautle  40049  elrfirn2  42666  wepwsolem  43013  kelac1  43034  islssfg2  43042  lnmlssfg  43051  onov0suclim  43245  relprel  44924  ovolval5lem3  46631  2elfz3nn0  47293  2elfz2melfz  47295  icceuelpartlem  47397  wtgoldbnnsum4prm  47764  bgoldbnnsum3prm  47766  bgoldbtbnd  47771  oppcendc  48941  setrec2fun  49504