Theorem mpan9 515

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 35	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	impcom 412	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sylan  591  vtocl2gf  3536  vtocl3gf  3537  vtocl2g  3538  vtocl3g  3539  sbcthdv  3760  elinsn  4676  axprlem4OLD  5401  swopolem  5579  wereu  5657  funssres  6580  dffv2  6976  fmptcof  7126  fnprb  7206  fntpb  7207  fliftfuns  7312  isorel  7324  oveqrspc2v  7437  caovclg  7602  caovcomg  7605  caovassg  7608  caovcang  7611  caovordig  7615  caovordg  7617  caovdig  7624  caovdirg  7627  caofidlcan  7712  peano5  7886  dmfexALT  7901  frpoins3xp3g  8133  fvmpocurryd  8263  qliftfuns  8798  nneneq  9186  ttrcltr  9681  ttrclselem2  9691  frins3  9723  cfslb  10245  hsmexlem4  10408  axdc3lem2  10430  axdc4lem  10434  adderpq  10936  mulerpq  10937  ltordlem  11734  lble  12162  uz11  12882  xrsupsslem  13328  xrinfmsslem  13329  xrsupss  13330  xrinfmss  13331  fseqsupubi  14010  hashbclem  14485  ccatass  14622  swrdswrd  14738  swrdccatin1  14758  swrdccatin2  14762  cshwcsh2id  14861  wwlktovf  14989  isercolllem1  15712  caucvgb  15727  zsum  15765  fsum  15767  fsumf1o  15770  fsumcvg2  15774  isummulc2  15809  fsum2dlem  15817  fsumcom2  15821  fsumshftm  15828  fsum0diag2  15830  fsum00  15846  fsumrlim  15859  o1fsum  15861  isumshft  15889  clim2prod  15938  ntrivcvgfvn0  15949  zprod  15987  fprod  15991  fprodf1o  15996  prodss  15997  fprodser  15999  fprodcllemf  16008  fprodm1s  16020  fprodp1s  16021  fprodabs  16024  fprod2dlem  16030  fprodcom2  16034  fprodefsum  16144  mod2eq1n2dvds  16400  sumeven  16440  lcmfun  16698  pythagtriplem4  16874  pcmptdvds  16949  prslem  18348  posi  18368  dlatmjdi  18574  lidrididd  18723  grpidinv2  19059  qsxpid  19238  ghmlin  19286  cntzmhm2  19407  dprdss  20096  dprd2d2  20111  omndadd  20193  srgrz  20284  srglz  20285  ringinvnz1ne0  20379  rrgeq0i  20798  lmodlema  20986  islmodd  20987  lsscl  21063  lsslss  21082  lspdisjb  21250  lsslinds  21981  assalem  22007  fvmptnn04if  23006  chfacfscmulgsum  23017  chfacfpmmulgsum  23021  ssnei2  23273  t1ficld  23484  t1sep2  23526  unconn  23586  1stcclb  23601  ptbasfi  23738  tx1stc  23807  qtoptop2  23856  r0sep  23905  ustincl  24365  ustdiag  24366  ustinvel  24367  ustexhalf  24368  psmet0  24465  psmettri2  24466  prdsdsf  24524  prdsxmet  24526  cncfi  25053  ovolfiniun  25660  mbfimaopnlem  25814  limciun  26053  dvcn  26080  dvmptfsum  26134  dvfsumle  26180  dvfsumabs  26182  dvfsumlem3  26187  itgsubst  26208  fsumvma  27377  dchrelbasd  27403  dchrisumlem3  27655  ssslts1  27966  ssslts2  27967  madeval2  28026  elmade  28050  axcontlem9  29322  usgruspgrb  29533  uspgrloopvtxel  29866  umgr2v2evtxel  29872  clwwlknonex2lem2  30459  3spthd  30527  grpoass  30855  lnolin  31106  elnlfn  32280  strlem4  32606  hstrlem4  32614  atmd  32751  nn0min  33165  slmdlema  33523  esumcvg  34476  measxun2  34600  sibfima  34728  bnj110  35246  bnj594  35300  bnj1491  35445  loop1cycl  35629  cvmcov  35755  mrsubcn  36011  dfon2lem5  36277  ifscgr  36536  nn0prpw  36834  neibastop2lem  36871  axnulregtco  36991  tr0el  36996  dfttc4  37041  bj-restb  37736  poimirlem25  38296  poimirlem32  38303  mbfresfi  38317  totbndss  38428  ghomlinOLD  38539  rngodi  38555  rngodir  38556  rngoass  38557  rngohomadd  38620  rngohommul  38621  crngocom  38652  idladdcl  38670  idllmulcl  38671  idlrmulcl  38672  exlimddvf  38770  oposlem  39956  cvlexch1  40102  hlsuprexch  40155  lautle  40858  elrfirn2  43427  wepwsolem  43769  kelac1  43790  islssfg2  43798  lnmlssfg  43807  onov0suclim  44001  relprel  45660  ovolval5lem3  47368  2elfz3nn0  48053  2elfz2melfz  48055  icceuelpartlem  48184  wtgoldbnnsum4prm  48567  bgoldbnnsum3prm  48569  bgoldbtbnd  48574  gpgedg2iv  48832  pgnbgreunbgrlem3  48883  pgnbgreunbgrlem6  48889  oppcendc  49796  setrec2fun  50470