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  580  vtocl2gf  3541  vtocl3gf  3542  vtocl2g  3543  vtocl3g  3544  vtoclegftOLD  3558  sbcthdv  3772  elinsn  4677  axprlem4OLD  5387  swopolem  5559  wereu  5637  funssres  6563  dffv2  6959  fmptcof  7105  fnprb  7185  fntpb  7186  fliftfuns  7292  isorel  7304  oveqrspc2v  7417  caovclg  7584  caovcomg  7587  caovassg  7590  caovcang  7593  caovordig  7597  caovordg  7599  caovdig  7606  caovdirg  7609  caofidlcan  7694  peano5  7872  dmfexALT  7887  frpoins3xp3g  8123  fvmpocurryd  8253  qliftfuns  8780  nneneq  9176  ttrcltr  9676  ttrclselem2  9686  frins3  9715  cfslb  10226  hsmexlem4  10389  axdc3lem2  10411  axdc4lem  10415  adderpq  10916  mulerpq  10917  ltordlem  11710  lble  12142  uz11  12825  xrsupsslem  13274  xrinfmsslem  13275  xrsupss  13276  xrinfmss  13277  fseqsupubi  13950  hashbclem  14424  ccatass  14560  swrdswrd  14677  swrdccatin1  14697  swrdccatin2  14701  cshwcsh2id  14801  wwlktovf  14929  isercolllem1  15638  caucvgb  15653  zsum  15691  fsum  15693  fsumf1o  15696  fsumcvg2  15700  isummulc2  15735  fsum2dlem  15743  fsumcom2  15747  fsumshftm  15754  fsum0diag2  15756  fsum00  15771  fsumrlim  15784  o1fsum  15786  isumshft  15812  clim2prod  15861  ntrivcvgfvn0  15872  zprod  15910  fprod  15914  fprodf1o  15919  prodss  15920  fprodser  15922  fprodcllemf  15931  fprodm1s  15943  fprodp1s  15944  fprodabs  15947  fprod2dlem  15953  fprodcom2  15957  fprodefsum  16068  mod2eq1n2dvds  16324  sumeven  16364  lcmfun  16622  pythagtriplem4  16797  pcmptdvds  16872  prslem  18265  posi  18285  dlatmjdi  18489  lidrididd  18604  grpidinv2  18936  ghmlin  19160  cntzmhm2  19281  dprdss  19968  dprd2d2  19983  srgrz  20123  srglz  20124  ringinvnz1ne0  20216  rrgeq0i  20615  lmodlema  20778  islmodd  20779  lsscl  20855  lsslss  20874  lspdisjb  21043  lsslinds  21747  assalem  21773  fvmptnn04if  22743  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  ssnei2  23010  t1ficld  23221  t1sep2  23263  unconn  23323  1stcclb  23338  ptbasfi  23475  tx1stc  23544  qtoptop2  23593  r0sep  23642  ustincl  24102  ustdiag  24103  ustinvel  24104  ustexhalf  24105  psmet0  24203  psmettri2  24204  prdsdsf  24262  prdsxmet  24264  cncfi  24794  ovolfiniun  25409  mbfimaopnlem  25563  limciun  25802  dvcn  25830  dvmptfsum  25886  dvfsumle  25933  dvfsumleOLD  25934  dvfsumabs  25936  dvfsumlem3  25942  itgsubst  25963  fsumvma  27131  dchrelbasd  27157  dchrisumlem3  27409  sssslt1  27714  sssslt2  27715  madeval2  27768  elmade  27786  axcontlem9  28906  usgruspgrb  29117  uspgrloopvtxel  29451  umgr2v2evtxel  29457  clwwlknonex2lem2  30044  3spthd  30112  grpoass  30439  lnolin  30690  elnlfn  31864  strlem4  32190  hstrlem4  32198  atmd  32335  nn0min  32752  omndadd  33027  slmdlema  33163  qsxpid  33340  esumcvg  34083  measxun2  34207  sibfima  34336  bnj110  34855  bnj594  34909  bnj1491  35054  loop1cycl  35131  cvmcov  35257  mrsubcn  35513  dfon2lem5  35782  ifscgr  36039  nn0prpw  36318  neibastop2lem  36355  bj-restb  37089  poimirlem25  37646  poimirlem32  37653  mbfresfi  37667  totbndss  37778  ghomlinOLD  37889  rngodi  37905  rngodir  37906  rngoass  37907  rngohomadd  37970  rngohommul  37971  crngocom  38002  idladdcl  38020  idllmulcl  38021  idlrmulcl  38022  exlimddvf  38122  oposlem  39182  cvlexch1  39328  hlsuprexch  39382  lautle  40085  elrfirn2  42691  wepwsolem  43038  kelac1  43059  islssfg2  43067  lnmlssfg  43076  onov0suclim  43270  relprel  44948  ovolval5lem3  46659  2elfz3nn0  47321  2elfz2melfz  47323  icceuelpartlem  47440  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  bgoldbtbnd  47814  gpgedg2iv  48062  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118  oppcendc  49011  setrec2fun  49685