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  3524  vtocl3gf  3525  vtocl2g  3526  vtocl3g  3527  sbcthdv  3753  elinsn  4664  axprlem4OLD  5371  swopolem  5539  wereu  5617  funssres  6533  dffv2  6926  fmptcof  7072  fnprb  7151  fntpb  7152  fliftfuns  7257  isorel  7269  oveqrspc2v  7382  caovclg  7547  caovcomg  7550  caovassg  7553  caovcang  7556  caovordig  7560  caovordg  7562  caovdig  7569  caovdirg  7572  caofidlcan  7657  peano5  7832  dmfexALT  7847  frpoins3xp3g  8080  fvmpocurryd  8210  qliftfuns  8737  nneneq  9126  ttrcltr  9617  ttrclselem2  9627  frins3  9659  cfslb  10168  hsmexlem4  10331  axdc3lem2  10353  axdc4lem  10357  adderpq  10858  mulerpq  10859  ltordlem  11653  lble  12085  uz11  12767  xrsupsslem  13213  xrinfmsslem  13214  xrsupss  13215  xrinfmss  13216  fseqsupubi  13892  hashbclem  14366  ccatass  14503  swrdswrd  14619  swrdccatin1  14639  swrdccatin2  14643  cshwcsh2id  14742  wwlktovf  14870  isercolllem1  15579  caucvgb  15594  zsum  15632  fsum  15634  fsumf1o  15637  fsumcvg2  15641  isummulc2  15676  fsum2dlem  15684  fsumcom2  15688  fsumshftm  15695  fsum0diag2  15697  fsum00  15712  fsumrlim  15725  o1fsum  15727  isumshft  15753  clim2prod  15802  ntrivcvgfvn0  15813  zprod  15851  fprod  15855  fprodf1o  15860  prodss  15861  fprodser  15863  fprodcllemf  15872  fprodm1s  15884  fprodp1s  15885  fprodabs  15888  fprod2dlem  15894  fprodcom2  15898  fprodefsum  16009  mod2eq1n2dvds  16265  sumeven  16305  lcmfun  16563  pythagtriplem4  16738  pcmptdvds  16813  prslem  18211  posi  18231  dlatmjdi  18437  lidrididd  18586  grpidinv2  18918  ghmlin  19141  cntzmhm2  19262  dprdss  19951  dprd2d2  19966  omndadd  20048  srgrz  20133  srglz  20134  ringinvnz1ne0  20226  rrgeq0i  20623  lmodlema  20807  islmodd  20808  lsscl  20884  lsslss  20903  lspdisjb  21072  lsslinds  21777  assalem  21803  fvmptnn04if  22784  chfacfscmulgsum  22795  chfacfpmmulgsum  22799  ssnei2  23051  t1ficld  23262  t1sep2  23304  unconn  23364  1stcclb  23379  ptbasfi  23516  tx1stc  23585  qtoptop2  23634  r0sep  23683  ustincl  24143  ustdiag  24144  ustinvel  24145  ustexhalf  24146  psmet0  24243  psmettri2  24244  prdsdsf  24302  prdsxmet  24304  cncfi  24834  ovolfiniun  25449  mbfimaopnlem  25603  limciun  25842  dvcn  25870  dvmptfsum  25926  dvfsumle  25973  dvfsumleOLD  25974  dvfsumabs  25976  dvfsumlem3  25982  itgsubst  26003  fsumvma  27171  dchrelbasd  27197  dchrisumlem3  27449  sssslt1  27756  sssslt2  27757  madeval2  27814  elmade  27832  axcontlem9  28971  usgruspgrb  29182  uspgrloopvtxel  29516  umgr2v2evtxel  29522  clwwlknonex2lem2  30109  3spthd  30177  grpoass  30504  lnolin  30755  elnlfn  31929  strlem4  32255  hstrlem4  32263  atmd  32400  nn0min  32829  slmdlema  33213  qsxpid  33371  esumcvg  34171  measxun2  34295  sibfima  34423  bnj110  34942  bnj594  34996  bnj1491  35141  loop1cycl  35253  cvmcov  35379  mrsubcn  35635  dfon2lem5  35901  ifscgr  36160  nn0prpw  36439  neibastop2lem  36476  bj-restb  37211  poimirlem25  37758  poimirlem32  37765  mbfresfi  37779  totbndss  37890  ghomlinOLD  38001  rngodi  38017  rngodir  38018  rngoass  38019  rngohomadd  38082  rngohommul  38083  crngocom  38114  idladdcl  38132  idllmulcl  38133  idlrmulcl  38134  exlimddvf  38234  oposlem  39354  cvlexch1  39500  hlsuprexch  39553  lautle  40256  elrfirn2  42853  wepwsolem  43199  kelac1  43220  islssfg2  43228  lnmlssfg  43237  onov0suclim  43431  relprel  45108  ovolval5lem3  46814  2elfz3nn0  47478  2elfz2melfz  47480  icceuelpartlem  47597  wtgoldbnnsum4prm  47964  bgoldbnnsum3prm  47966  bgoldbtbnd  47971  gpgedg2iv  48229  pgnbgreunbgrlem3  48280  pgnbgreunbgrlem6  48286  oppcendc  49179  setrec2fun  49853