Theorem mpan9 516

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 413	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylan  592  vtocl2gf  3531  vtocl3gf  3532  vtocl2g  3533  vtocl3g  3534  sbcthdv  3755  elinsn  4671  axprlem4OLD  5395  swopolem  5573  wereu  5651  funssres  6577  dffv2  6973  fmptcof  7124  fnprb  7207  fntpb  7208  fliftfuns  7315  isorel  7327  oveqrspc2v  7440  caovclg  7606  caovcomg  7609  caovassg  7612  caovcang  7615  caovordig  7619  caovordg  7621  caovdig  7628  caovdirg  7631  caofidlcan  7716  peano5  7890  dmfexALT  7905  frpoins3xp3g  8139  fvmpocurryd  8269  qliftfuns  8804  nneneq  9200  ttrcltr  9695  ttrclselem2  9705  frins3  9737  cfslb  10268  hsmexlem4  10431  axdc3lem2  10453  axdc4lem  10457  adderpq  10965  mulerpq  10966  ltordlem  11763  lble  12191  uz11  12912  xrsupsslem  13359  xrinfmsslem  13360  xrsupss  13361  xrinfmss  13362  fseqsupubi  14042  hashbclem  14517  ccatass  14654  swrdswrd  14774  swrdccatin1  14794  swrdccatin2  14798  cshwcsh2id  14899  wwlktovf  15029  isercolllem1  15752  caucvgb  15767  zsum  15804  fsum  15806  fsumf1o  15809  fsumcvg2  15813  isummulc2  15848  fsum2dlem  15856  fsumcom2  15860  fsumshftm  15867  fsum0diag2  15869  fsum00  15885  fsumrlim  15898  o1fsum  15900  isumshft  15928  clim2prod  15977  ntrivcvgfvn0  15988  zprod  16024  fprod  16028  fprodf1o  16033  prodss  16034  fprodser  16036  fprodcllemf  16045  fprodm1s  16057  fprodp1s  16058  fprodabs  16061  fprod2dlem  16067  fprodcom2  16071  fprodefsum  16181  mod2eq1n2dvds  16437  sumeven  16477  sumodd  16478  lcmfun  16735  pythagtriplem4  16911  pcmptdvds  16986  prslem  18385  posi  18405  dlatmjdi  18611  lidrididd  18764  grpidinv2  19121  qsxpid  19300  ghmlin  19348  cntzmhm2  19469  dprdss  20158  dprd2d2  20173  omndadd  20255  srgrz  20346  srglz  20347  ringinvnz1ne0  20442  rrgeq0i  20861  lmodlema  21049  islmodd  21050  lsscl  21126  lsslss  21145  lspdisjb  21313  lsslinds  22044  assalem  22072  fvmptnn04if  23074  chfacfscmulgsum  23085  chfacfpmmulgsum  23089  ssnei2  23341  t1ficld  23552  t1sep2  23594  unconn  23654  1stcclb  23669  ptbasfi  23807  tx1stc  23876  qtoptop2  23925  r0sep  23974  ustincl  24434  ustdiag  24435  ustinvel  24436  ustexhalf  24437  psmet0  24534  psmettri2  24535  prdsdsf  24593  prdsxmet  24595  cncfi  25122  ovolfiniun  25729  mbfimaopnlem  25883  limciun  26121  dvcn  26148  dvmptfsum  26202  dvfsumle  26248  dvfsumabs  26250  dvfsumlem3  26255  itgsubst  26276  fsumvma  27449  dchrelbasd  27475  dchrisumlem3  27727  ssslts1  28038  ssslts2  28039  madeval2  28098  elmade  28122  axcontlem9  29429  usgruspgrb  29643  uspgrloopvtxel  29976  umgr2v2evtxel  29982  clwwlknonex2lem2  30578  loop1cycl  30623  3spthd  30656  grpoass  30984  lnolin  31235  elnlfn  32409  strlem4  32735  hstrlem4  32743  atmd  32880  nn0min  33291  slmdlema  33643  esumcvg  34596  measxun2  34721  sibfima  34849  bnj110  35367  bnj594  35421  bnj1491  35566  cvmcov  35842  mrsubcn  36098  dfon2lem5  36364  ifscgr  36624  nn0prpw  36942  neibastop2lem  36979  axnulregtco  37099  tr0el  37104  dfttc4  37149  bj-restb  37844  poimirlem25  38394  poimirlem32  38401  mbfresfi  38415  totbndss  38527  ghomlinOLD  38638  rngodi  38654  rngodir  38655  rngoass  38656  rngohomadd  38719  rngohommul  38720  crngocom  38751  idladdcl  38769  idllmulcl  38770  idlrmulcl  38771  exlimddvf  38869  oposlem  40055  cvlexch1  40201  hlsuprexch  40254  lautle  40957  elrfirn2  43541  wepwsolem  43883  kelac1  43904  islssfg2  43912  lnmlssfg  43921  onov0suclim  44115  relprel  45774  ovolval5lem3  47482  2elfz3nn0  48204  2elfz2melfz  48206  icceuelpartlem  48335  wtgoldbnnsum4prm  48718  bgoldbnnsum3prm  48720  bgoldbtbnd  48725  gpgedg2iv  48983  pgnbgreunbgrlem3  49034  pgnbgreunbgrlem6  49040  oppcendc  49944  setrec2fun  50618