Theorem mpan9 511

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  sylan  586  vtocl2gf  3515  vtocl3gf  3516  vtocl2g  3517  vtocl3g  3518  sbcthdv  3739  elinsn  4642  axprlem4OLD  5359  swopolem  5536  wereu  5614  funssres  6529  dffv2  6922  fmptcof  7072  fnprb  7152  fntpb  7153  fliftfuns  7258  isorel  7270  oveqrspc2v  7383  caovclg  7548  caovcomg  7551  caovassg  7554  caovcang  7557  caovordig  7561  caovordg  7563  caovdig  7570  caovdirg  7573  caofidlcan  7658  peano5  7833  dmfexALT  7848  frpoins3xp3g  8081  fvmpocurryd  8211  qliftfuns  8741  nneneq  9130  ttrcltr  9628  ttrclselem2  9638  frins3  9670  cfslb  10179  hsmexlem4  10342  axdc3lem2  10364  axdc4lem  10368  adderpq  10870  mulerpq  10871  ltordlem  11666  lble  12099  uz11  12804  xrsupsslem  13250  xrinfmsslem  13251  xrsupss  13252  xrinfmss  13253  fseqsupubi  13931  hashbclem  14405  ccatass  14542  swrdswrd  14658  swrdccatin1  14678  swrdccatin2  14682  cshwcsh2id  14781  wwlktovf  14909  isercolllem1  15618  caucvgb  15633  zsum  15671  fsum  15673  fsumf1o  15676  fsumcvg2  15680  isummulc2  15715  fsum2dlem  15723  fsumcom2  15727  fsumshftm  15734  fsum0diag2  15736  fsum00  15752  fsumrlim  15765  o1fsum  15767  isumshft  15795  clim2prod  15844  ntrivcvgfvn0  15855  zprod  15893  fprod  15897  fprodf1o  15902  prodss  15903  fprodser  15905  fprodcllemf  15914  fprodm1s  15926  fprodp1s  15927  fprodabs  15930  fprod2dlem  15936  fprodcom2  15940  fprodefsum  16051  mod2eq1n2dvds  16307  sumeven  16347  lcmfun  16605  pythagtriplem4  16781  pcmptdvds  16856  prslem  18254  posi  18274  dlatmjdi  18480  lidrididd  18629  grpidinv2  18964  ghmlin  19187  cntzmhm2  19308  dprdss  19997  dprd2d2  20012  omndadd  20094  srgrz  20179  srglz  20180  ringinvnz1ne0  20272  rrgeq0i  20671  lmodlema  20855  islmodd  20856  lsscl  20932  lsslss  20951  lspdisjb  21119  lsslinds  21806  assalem  21832  fvmptnn04if  22832  chfacfscmulgsum  22843  chfacfpmmulgsum  22847  ssnei2  23099  t1ficld  23310  t1sep2  23352  unconn  23412  1stcclb  23427  ptbasfi  23564  tx1stc  23633  qtoptop2  23682  r0sep  23731  ustincl  24191  ustdiag  24192  ustinvel  24193  ustexhalf  24194  psmet0  24291  psmettri2  24292  prdsdsf  24350  prdsxmet  24352  cncfi  24879  ovolfiniun  25486  mbfimaopnlem  25640  limciun  25879  dvcn  25906  dvmptfsum  25960  dvfsumle  26006  dvfsumabs  26008  dvfsumlem3  26013  itgsubst  26034  fsumvma  27194  dchrelbasd  27220  dchrisumlem3  27472  ssslts1  27783  ssslts2  27784  madeval2  27843  elmade  27867  axcontlem9  29059  usgruspgrb  29270  uspgrloopvtxel  29603  umgr2v2evtxel  29609  clwwlknonex2lem2  30196  3spthd  30264  grpoass  30592  lnolin  30843  elnlfn  32017  strlem4  32343  hstrlem4  32351  atmd  32488  nn0min  32913  slmdlema  33284  qsxpid  33445  esumcvg  34270  measxun2  34394  sibfima  34522  bnj110  35040  bnj594  35094  bnj1491  35239  loop1cycl  35365  cvmcov  35491  mrsubcn  35747  dfon2lem5  36013  ifscgr  36272  nn0prpw  36551  neibastop2lem  36588  axnulregtco  36708  tr0el  36713  dfttc4  36758  bj-restb  37452  poimirlem25  38012  poimirlem32  38019  mbfresfi  38033  totbndss  38144  ghomlinOLD  38255  rngodi  38271  rngodir  38272  rngoass  38273  rngohomadd  38336  rngohommul  38337  crngocom  38368  idladdcl  38386  idllmulcl  38387  idlrmulcl  38388  exlimddvf  38488  oposlem  39674  cvlexch1  39820  hlsuprexch  39873  lautle  40576  elrfirn2  43145  wepwsolem  43487  kelac1  43508  islssfg2  43516  lnmlssfg  43525  onov0suclim  43719  relprel  45395  ovolval5lem3  47097  2elfz3nn0  47779  2elfz2melfz  47781  icceuelpartlem  47910  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  bgoldbtbnd  48300  gpgedg2iv  48558  pgnbgreunbgrlem3  48609  pgnbgreunbgrlem6  48615  oppcendc  49508  setrec2fun  50182