Theorem mpan9 502

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 398	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  sylan  575  vtocl2gf  3468  vtocl3gf  3469  vtocl2g  3470  vtoclegft  3481  sbcthdv  3667  elinsn  4476  swopolem  5283  wereu  5351  funssres  6178  dffv2  6531  fmptcof  6662  fnprb  6744  fntpb  6745  fliftfuns  6836  isorel  6848  oveqrspc2v  6949  caovclg  7103  caovcomg  7106  caovassg  7109  caovcang  7112  caovordig  7116  caovordg  7118  caovdig  7125  caovdirg  7128  peano5  7367  fvmpt2curryd  7679  qliftfuns  8117  nneneq  8431  cfslb  9423  hsmexlem4  9586  axdc3lem2  9608  axdc4lem  9612  adderpq  10113  mulerpq  10114  ltordlem  10900  lble  11329  uz11  12015  xrsupsslem  12449  xrinfmsslem  12450  xrsupss  12451  xrinfmss  12452  fseqsupubi  13096  hashbclem  13550  swrdswrd  13814  swrdccatin2  13856  cshwcsh2id  13979  wwlktovf  14108  isercolllem1  14803  caucvgb  14818  zsum  14856  fsum  14858  fsumf1o  14861  fsumcvg2  14865  isummulc2  14898  fsum2dlem  14906  fsumcom2  14910  fsumshftm  14917  fsum0diag2  14919  fsum00  14934  fsumrlim  14947  o1fsum  14949  isumshft  14975  clim2prod  15023  ntrivcvgfvn0  15034  zprod  15070  fprod  15074  fprodf1o  15079  prodss  15080  fprodser  15082  fprodcllemf  15091  fprodm1s  15103  fprodp1s  15104  fprodabs  15107  fprod2dlem  15113  fprodcom2  15117  fprodefsum  15227  mod2eq1n2dvds  15475  sumeven  15517  lcmfun  15764  pythagtriplem4  15928  pcmptdvds  16002  prslem  17317  posi  17336  dlatmjdi  17580  grpidinv2  17861  ghmlin  18049  cntzmhm2  18155  dprdss  18815  dprd2d2  18830  srgrz  18913  srglz  18914  ringinvnz1ne0  18979  lmodlema  19260  islmodd  19261  lsscl  19335  lsslss  19356  lspdisjb  19521  rrgeq0i  19686  assalem  19713  lsslinds  20574  fvmptnn04if  21061  chfacfscmulgsum  21072  chfacfpmmulgsum  21076  ssnei2  21328  t1ficld  21539  t1sep2  21581  unconn  21641  1stcclb  21656  ptbasfi  21793  tx1stc  21862  qtoptop2  21911  r0sep  21960  ustincl  22419  ustdiag  22420  ustinvel  22421  ustexhalf  22422  psmet0  22521  psmettri2  22522  prdsdsf  22580  prdsxmet  22582  cncfi  23105  ovolfiniun  23705  mbfimaopnlem  23859  limciun  24095  dvcn  24121  dvmptfsum  24175  dvfsumle  24221  dvfsumabs  24223  dvfsumlem3  24228  itgsubst  24249  fsumvma  25390  dchrelbasd  25416  dchrisumlem3  25632  axcontlem9  26321  usgruspgrb  26530  uspgrloopvtxel  26864  umgr2v2evtxel  26870  clwwlknonex2lem2  27510  3spthd  27579  grpoass  27930  lnolin  28181  elnlfn  29359  strlem4  29685  hstrlem4  29693  atmd  29830  nn0min  30131  omndadd  30268  slmdlema  30318  esumcvg  30746  measxun2  30871  sibfima  30998  bnj110  31527  bnj594  31581  bnj1491  31724  cvmcov  31844  mrsubcn  32015  dfon2lem5  32280  sssslt1  32495  madeval2  32525  ifscgr  32740  nn0prpw  32906  neibastop2lem  32943  bj-restb  33620  poimirlem25  34044  poimirlem32  34051  mbfresfi  34065  totbndss  34184  ghomlinOLD  34295  rngodi  34311  rngodir  34312  rngoass  34313  rngohomadd  34376  rngohommul  34377  crngocom  34408  idladdcl  34426  idllmulcl  34427  idlrmulcl  34428  exlimddvf  34532  oposlem  35320  cvlexch1  35466  hlsuprexch  35519  lautle  36222  elrfirn2  38201  wepwsolem  38553  kelac1  38574  islssfg2  38582  lnmlssfg  38591  2elfz3nn0  42340  2elfz2melfz  42342  icceuelpartlem  42385  wtgoldbnnsum4prm  42697  bgoldbnnsum3prm  42699  bgoldbtbnd  42704  setrec2fun  43526