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  581  vtocl2gf  3515  vtocl3gf  3516  vtocl2g  3517  vtocl3g  3518  sbcthdv  3744  elinsn  4654  axprlem4OLD  5372  swopolem  5549  wereu  5627  funssres  6542  dffv2  6935  fmptcof  7083  fnprb  7163  fntpb  7164  fliftfuns  7269  isorel  7281  oveqrspc2v  7394  caovclg  7559  caovcomg  7562  caovassg  7565  caovcang  7568  caovordig  7572  caovordg  7574  caovdig  7581  caovdirg  7584  caofidlcan  7669  peano5  7844  dmfexALT  7859  frpoins3xp3g  8091  fvmpocurryd  8221  qliftfuns  8751  nneneq  9140  ttrcltr  9637  ttrclselem2  9647  frins3  9679  cfslb  10188  hsmexlem4  10351  axdc3lem2  10373  axdc4lem  10377  adderpq  10879  mulerpq  10880  ltordlem  11675  lble  12108  uz11  12813  xrsupsslem  13259  xrinfmsslem  13260  xrsupss  13261  xrinfmss  13262  fseqsupubi  13940  hashbclem  14414  ccatass  14551  swrdswrd  14667  swrdccatin1  14687  swrdccatin2  14691  cshwcsh2id  14790  wwlktovf  14918  isercolllem1  15627  caucvgb  15642  zsum  15680  fsum  15682  fsumf1o  15685  fsumcvg2  15689  isummulc2  15724  fsum2dlem  15732  fsumcom2  15736  fsumshftm  15743  fsum0diag2  15745  fsum00  15761  fsumrlim  15774  o1fsum  15776  isumshft  15804  clim2prod  15853  ntrivcvgfvn0  15864  zprod  15902  fprod  15906  fprodf1o  15911  prodss  15912  fprodser  15914  fprodcllemf  15923  fprodm1s  15935  fprodp1s  15936  fprodabs  15939  fprod2dlem  15945  fprodcom2  15949  fprodefsum  16060  mod2eq1n2dvds  16316  sumeven  16356  lcmfun  16614  pythagtriplem4  16790  pcmptdvds  16865  prslem  18263  posi  18283  dlatmjdi  18489  lidrididd  18638  grpidinv2  18973  ghmlin  19196  cntzmhm2  19317  dprdss  20006  dprd2d2  20021  omndadd  20103  srgrz  20188  srglz  20189  ringinvnz1ne0  20281  rrgeq0i  20676  lmodlema  20860  islmodd  20861  lsscl  20937  lsslss  20956  lspdisjb  21124  lsslinds  21811  assalem  21837  fvmptnn04if  22814  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  ssnei2  23081  t1ficld  23292  t1sep2  23334  unconn  23394  1stcclb  23409  ptbasfi  23546  tx1stc  23615  qtoptop2  23664  r0sep  23713  ustincl  24173  ustdiag  24174  ustinvel  24175  ustexhalf  24176  psmet0  24273  psmettri2  24274  prdsdsf  24332  prdsxmet  24334  cncfi  24861  ovolfiniun  25468  mbfimaopnlem  25622  limciun  25861  dvcn  25888  dvmptfsum  25942  dvfsumle  25988  dvfsumabs  25990  dvfsumlem3  25995  itgsubst  26016  fsumvma  27176  dchrelbasd  27202  dchrisumlem3  27454  ssslts1  27765  ssslts2  27766  madeval2  27825  elmade  27849  axcontlem9  29041  usgruspgrb  29252  uspgrloopvtxel  29585  umgr2v2evtxel  29591  clwwlknonex2lem2  30178  3spthd  30246  grpoass  30574  lnolin  30825  elnlfn  31999  strlem4  32325  hstrlem4  32333  atmd  32470  nn0min  32894  slmdlema  33264  qsxpid  33422  esumcvg  34230  measxun2  34354  sibfima  34482  bnj110  35000  bnj594  35054  bnj1491  35199  loop1cycl  35319  cvmcov  35445  mrsubcn  35701  dfon2lem5  35967  ifscgr  36226  nn0prpw  36505  neibastop2lem  36542  axnulregtco  36662  tr0el  36667  dfttc4  36712  bj-restb  37406  poimirlem25  37966  poimirlem32  37973  mbfresfi  37987  totbndss  38098  ghomlinOLD  38209  rngodi  38225  rngodir  38226  rngoass  38227  rngohomadd  38290  rngohommul  38291  crngocom  38322  idladdcl  38340  idllmulcl  38341  idlrmulcl  38342  exlimddvf  38442  oposlem  39628  cvlexch1  39774  hlsuprexch  39827  lautle  40530  elrfirn2  43128  wepwsolem  43470  kelac1  43491  islssfg2  43499  lnmlssfg  43508  onov0suclim  43702  relprel  45378  ovolval5lem3  47082  2elfz3nn0  47764  2elfz2melfz  47766  icceuelpartlem  47895  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  bgoldbtbnd  48285  gpgedg2iv  48543  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem6  48600  oppcendc  49493  setrec2fun  50167