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  3529  vtocl3gf  3530  vtocl2g  3531  vtocl3g  3532  vtoclegftOLD  3546  sbcthdv  3760  elinsn  4664  axprlem4OLD  5371  swopolem  5541  wereu  5619  funssres  6530  dffv2  6922  fmptcof  7068  fnprb  7148  fntpb  7149  fliftfuns  7255  isorel  7267  oveqrspc2v  7380  caovclg  7545  caovcomg  7548  caovassg  7551  caovcang  7554  caovordig  7558  caovordg  7560  caovdig  7567  caovdirg  7570  caofidlcan  7655  peano5  7833  dmfexALT  7848  frpoins3xp3g  8081  fvmpocurryd  8211  qliftfuns  8738  nneneq  9130  ttrcltr  9631  ttrclselem2  9641  frins3  9670  cfslb  10179  hsmexlem4  10342  axdc3lem2  10364  axdc4lem  10368  adderpq  10869  mulerpq  10870  ltordlem  11664  lble  12096  uz11  12779  xrsupsslem  13228  xrinfmsslem  13229  xrsupss  13230  xrinfmss  13231  fseqsupubi  13904  hashbclem  14378  ccatass  14514  swrdswrd  14630  swrdccatin1  14650  swrdccatin2  14654  cshwcsh2id  14754  wwlktovf  14882  isercolllem1  15591  caucvgb  15606  zsum  15644  fsum  15646  fsumf1o  15649  fsumcvg2  15653  isummulc2  15688  fsum2dlem  15696  fsumcom2  15700  fsumshftm  15707  fsum0diag2  15709  fsum00  15724  fsumrlim  15737  o1fsum  15739  isumshft  15765  clim2prod  15814  ntrivcvgfvn0  15825  zprod  15863  fprod  15867  fprodf1o  15872  prodss  15873  fprodser  15875  fprodcllemf  15884  fprodm1s  15896  fprodp1s  15897  fprodabs  15900  fprod2dlem  15906  fprodcom2  15910  fprodefsum  16021  mod2eq1n2dvds  16277  sumeven  16317  lcmfun  16575  pythagtriplem4  16750  pcmptdvds  16825  prslem  18222  posi  18242  dlatmjdi  18448  lidrididd  18563  grpidinv2  18895  ghmlin  19119  cntzmhm2  19240  dprdss  19929  dprd2d2  19944  omndadd  20026  srgrz  20111  srglz  20112  ringinvnz1ne0  20204  rrgeq0i  20603  lmodlema  20787  islmodd  20788  lsscl  20864  lsslss  20883  lspdisjb  21052  lsslinds  21757  assalem  21783  fvmptnn04if  22753  chfacfscmulgsum  22764  chfacfpmmulgsum  22768  ssnei2  23020  t1ficld  23231  t1sep2  23273  unconn  23333  1stcclb  23348  ptbasfi  23485  tx1stc  23554  qtoptop2  23603  r0sep  23652  ustincl  24112  ustdiag  24113  ustinvel  24114  ustexhalf  24115  psmet0  24213  psmettri2  24214  prdsdsf  24272  prdsxmet  24274  cncfi  24804  ovolfiniun  25419  mbfimaopnlem  25573  limciun  25812  dvcn  25840  dvmptfsum  25896  dvfsumle  25943  dvfsumleOLD  25944  dvfsumabs  25946  dvfsumlem3  25952  itgsubst  25973  fsumvma  27141  dchrelbasd  27167  dchrisumlem3  27419  sssslt1  27725  sssslt2  27726  madeval2  27782  elmade  27800  axcontlem9  28936  usgruspgrb  29147  uspgrloopvtxel  29481  umgr2v2evtxel  29487  clwwlknonex2lem2  30071  3spthd  30139  grpoass  30466  lnolin  30717  elnlfn  31891  strlem4  32217  hstrlem4  32225  atmd  32362  nn0min  32784  slmdlema  33164  qsxpid  33318  esumcvg  34072  measxun2  34196  sibfima  34325  bnj110  34844  bnj594  34898  bnj1491  35043  loop1cycl  35129  cvmcov  35255  mrsubcn  35511  dfon2lem5  35780  ifscgr  36037  nn0prpw  36316  neibastop2lem  36353  bj-restb  37087  poimirlem25  37644  poimirlem32  37651  mbfresfi  37665  totbndss  37776  ghomlinOLD  37887  rngodi  37903  rngodir  37904  rngoass  37905  rngohomadd  37968  rngohommul  37969  crngocom  38000  idladdcl  38018  idllmulcl  38019  idlrmulcl  38020  exlimddvf  38120  oposlem  39180  cvlexch1  39326  hlsuprexch  39380  lautle  40083  elrfirn2  42689  wepwsolem  43035  kelac1  43056  islssfg2  43064  lnmlssfg  43073  onov0suclim  43267  relprel  44945  ovolval5lem3  46655  2elfz3nn0  47320  2elfz2melfz  47322  icceuelpartlem  47439  wtgoldbnnsum4prm  47806  bgoldbnnsum3prm  47808  bgoldbtbnd  47813  gpgedg2iv  48071  pgnbgreunbgrlem3  48122  pgnbgreunbgrlem6  48128  oppcendc  49023  setrec2fun  49697