Theorem mpan9 515

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 35	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	impcom 412	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sylan  591  vtocl2gf  3545  vtocl3gf  3546  vtocl2g  3547  vtocl3g  3548  sbcthdv  3769  elinsn  4678  axprlem4OLD  5399  swopolem  5577  wereu  5655  funssres  6578  dffv2  6974  fmptcof  7124  fnprb  7204  fntpb  7205  fliftfuns  7310  isorel  7322  oveqrspc2v  7435  caovclg  7600  caovcomg  7603  caovassg  7606  caovcang  7609  caovordig  7613  caovordg  7615  caovdig  7622  caovdirg  7625  caofidlcan  7710  peano5  7886  dmfexALT  7901  frpoins3xp3g  8133  fvmpocurryd  8263  qliftfuns  8798  nneneq  9186  ttrcltr  9681  ttrclselem2  9691  frins3  9723  cfslb  10246  hsmexlem4  10409  axdc3lem2  10431  axdc4lem  10435  adderpq  10937  mulerpq  10938  ltordlem  11735  lble  12163  uz11  12883  xrsupsslem  13329  xrinfmsslem  13330  xrsupss  13331  xrinfmss  13332  fseqsupubi  14010  hashbclem  14485  ccatass  14622  swrdswrd  14738  swrdccatin1  14758  swrdccatin2  14762  cshwcsh2id  14861  wwlktovf  14989  isercolllem1  15712  caucvgb  15727  zsum  15765  fsum  15767  fsumf1o  15770  fsumcvg2  15774  isummulc2  15809  fsum2dlem  15817  fsumcom2  15821  fsumshftm  15828  fsum0diag2  15830  fsum00  15846  fsumrlim  15859  o1fsum  15861  isumshft  15889  clim2prod  15938  ntrivcvgfvn0  15949  zprod  15987  fprod  15991  fprodf1o  15996  prodss  15997  fprodser  15999  fprodcllemf  16008  fprodm1s  16020  fprodp1s  16021  fprodabs  16024  fprod2dlem  16030  fprodcom2  16034  fprodefsum  16145  mod2eq1n2dvds  16401  sumeven  16441  lcmfun  16699  pythagtriplem4  16875  pcmptdvds  16950  prslem  18349  posi  18369  dlatmjdi  18575  lidrididd  18724  grpidinv2  19060  qsxpid  19239  ghmlin  19287  cntzmhm2  19408  dprdss  20097  dprd2d2  20112  omndadd  20194  srgrz  20285  srglz  20286  ringinvnz1ne0  20379  rrgeq0i  20780  lmodlema  20960  islmodd  20961  lsscl  21037  lsslss  21056  lspdisjb  21224  lsslinds  21946  assalem  21972  fvmptnn04if  22971  chfacfscmulgsum  22982  chfacfpmmulgsum  22986  ssnei2  23238  t1ficld  23449  t1sep2  23491  unconn  23551  1stcclb  23566  ptbasfi  23703  tx1stc  23772  qtoptop2  23821  r0sep  23870  ustincl  24330  ustdiag  24331  ustinvel  24332  ustexhalf  24333  psmet0  24430  psmettri2  24431  prdsdsf  24489  prdsxmet  24491  cncfi  25018  ovolfiniun  25625  mbfimaopnlem  25779  limciun  26018  dvcn  26045  dvmptfsum  26099  dvfsumle  26145  dvfsumabs  26147  dvfsumlem3  26152  itgsubst  26173  fsumvma  27339  dchrelbasd  27365  dchrisumlem3  27617  ssslts1  27928  ssslts2  27929  madeval2  27988  elmade  28012  axcontlem9  29259  usgruspgrb  29470  uspgrloopvtxel  29803  umgr2v2evtxel  29809  clwwlknonex2lem2  30396  3spthd  30464  grpoass  30792  lnolin  31043  elnlfn  32217  strlem4  32543  hstrlem4  32551  atmd  32688  nn0min  33102  slmdlema  33460  esumcvg  34417  measxun2  34541  sibfima  34669  bnj110  35187  bnj594  35241  bnj1491  35386  loop1cycl  35524  cvmcov  35650  mrsubcn  35906  dfon2lem5  36172  ifscgr  36431  nn0prpw  36719  neibastop2lem  36756  axnulregtco  36876  tr0el  36881  dfttc4  36926  bj-restb  37619  poimirlem25  38179  poimirlem32  38186  mbfresfi  38200  totbndss  38311  ghomlinOLD  38422  rngodi  38438  rngodir  38439  rngoass  38440  rngohomadd  38503  rngohommul  38504  crngocom  38535  idladdcl  38553  idllmulcl  38554  idlrmulcl  38555  exlimddvf  38655  oposlem  39841  cvlexch1  39987  hlsuprexch  40040  lautle  40743  elrfirn2  43314  wepwsolem  43656  kelac1  43677  islssfg2  43685  lnmlssfg  43694  onov0suclim  43888  relprel  45547  ovolval5lem3  47255  2elfz3nn0  47937  2elfz2melfz  47939  icceuelpartlem  48068  wtgoldbnnsum4prm  48451  bgoldbnnsum3prm  48453  bgoldbtbnd  48458  gpgedg2iv  48716  pgnbgreunbgrlem3  48767  pgnbgreunbgrlem6  48773  oppcendc  49676  setrec2fun  50350