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  3516  vtocl3gf  3517  vtocl2g  3518  vtocl3g  3519  sbcthdv  3745  elinsn  4655  axprlem4OLD  5365  swopolem  5540  wereu  5618  funssres  6534  dffv2  6927  fmptcof  7075  fnprb  7154  fntpb  7155  fliftfuns  7260  isorel  7272  oveqrspc2v  7385  caovclg  7550  caovcomg  7553  caovassg  7556  caovcang  7559  caovordig  7563  caovordg  7565  caovdig  7572  caovdirg  7575  caofidlcan  7660  peano5  7835  dmfexALT  7850  frpoins3xp3g  8082  fvmpocurryd  8212  qliftfuns  8742  nneneq  9131  ttrcltr  9626  ttrclselem2  9636  frins3  9668  cfslb  10177  hsmexlem4  10340  axdc3lem2  10362  axdc4lem  10366  adderpq  10868  mulerpq  10869  ltordlem  11663  lble  12095  uz11  12777  xrsupsslem  13223  xrinfmsslem  13224  xrsupss  13225  xrinfmss  13226  fseqsupubi  13902  hashbclem  14376  ccatass  14513  swrdswrd  14629  swrdccatin1  14649  swrdccatin2  14653  cshwcsh2id  14752  wwlktovf  14880  isercolllem1  15589  caucvgb  15604  zsum  15642  fsum  15644  fsumf1o  15647  fsumcvg2  15651  isummulc2  15686  fsum2dlem  15694  fsumcom2  15698  fsumshftm  15705  fsum0diag2  15707  fsum00  15722  fsumrlim  15735  o1fsum  15737  isumshft  15763  clim2prod  15812  ntrivcvgfvn0  15823  zprod  15861  fprod  15865  fprodf1o  15870  prodss  15871  fprodser  15873  fprodcllemf  15882  fprodm1s  15894  fprodp1s  15895  fprodabs  15898  fprod2dlem  15904  fprodcom2  15908  fprodefsum  16019  mod2eq1n2dvds  16275  sumeven  16315  lcmfun  16573  pythagtriplem4  16748  pcmptdvds  16823  prslem  18221  posi  18241  dlatmjdi  18447  lidrididd  18596  grpidinv2  18931  ghmlin  19154  cntzmhm2  19275  dprdss  19964  dprd2d2  19979  omndadd  20061  srgrz  20146  srglz  20147  ringinvnz1ne0  20239  rrgeq0i  20634  lmodlema  20818  islmodd  20819  lsscl  20895  lsslss  20914  lspdisjb  21083  lsslinds  21788  assalem  21814  fvmptnn04if  22792  chfacfscmulgsum  22803  chfacfpmmulgsum  22807  ssnei2  23059  t1ficld  23270  t1sep2  23312  unconn  23372  1stcclb  23387  ptbasfi  23524  tx1stc  23593  qtoptop2  23642  r0sep  23691  ustincl  24151  ustdiag  24152  ustinvel  24153  ustexhalf  24154  psmet0  24251  psmettri2  24252  prdsdsf  24310  prdsxmet  24312  cncfi  24839  ovolfiniun  25446  mbfimaopnlem  25600  limciun  25839  dvcn  25866  dvmptfsum  25920  dvfsumle  25967  dvfsumleOLD  25968  dvfsumabs  25970  dvfsumlem3  25976  itgsubst  25997  fsumvma  27164  dchrelbasd  27190  dchrisumlem3  27442  ssslts1  27753  ssslts2  27754  madeval2  27813  elmade  27837  axcontlem9  29029  usgruspgrb  29240  uspgrloopvtxel  29574  umgr2v2evtxel  29580  clwwlknonex2lem2  30167  3spthd  30235  grpoass  30563  lnolin  30814  elnlfn  31988  strlem4  32314  hstrlem4  32322  atmd  32459  nn0min  32884  slmdlema  33269  qsxpid  33427  esumcvg  34236  measxun2  34360  sibfima  34488  bnj110  35006  bnj594  35060  bnj1491  35205  loop1cycl  35325  cvmcov  35451  mrsubcn  35707  dfon2lem5  35973  ifscgr  36232  nn0prpw  36511  neibastop2lem  36548  axnultcoreg  36668  tr0el  36673  dfttc4  36718  bj-restb  37404  poimirlem25  37957  poimirlem32  37964  mbfresfi  37978  totbndss  38089  ghomlinOLD  38200  rngodi  38216  rngodir  38217  rngoass  38218  rngohomadd  38281  rngohommul  38282  crngocom  38313  idladdcl  38331  idllmulcl  38332  idlrmulcl  38333  exlimddvf  38433  oposlem  39619  cvlexch1  39765  hlsuprexch  39818  lautle  40521  elrfirn2  43127  wepwsolem  43473  kelac1  43494  islssfg2  43502  lnmlssfg  43511  onov0suclim  43705  relprel  45381  ovolval5lem3  47086  2elfz3nn0  47750  2elfz2melfz  47752  icceuelpartlem  47869  wtgoldbnnsum4prm  48236  bgoldbnnsum3prm  48238  bgoldbtbnd  48243  gpgedg2iv  48501  pgnbgreunbgrlem3  48552  pgnbgreunbgrlem6  48558  oppcendc  49451  setrec2fun  50125