Theorem mpan9 505

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  sylan  578  vtocl2gf  3553  vtocl3gf  3554  vtocl2g  3555  vtocl3g  3556  vtoclegftOLD  3571  sbcthdv  3792  elinsn  4719  axprlem4  5430  swopolem  5604  wereu  5678  funssres  6603  dffv2  6997  fmptcof  7144  fnprb  7225  fntpb  7226  fliftfuns  7326  isorel  7338  oveqrspc2v  7451  caovclg  7618  caovcomg  7621  caovassg  7624  caovcang  7627  caovordig  7631  caovordg  7633  caovdig  7640  caovdirg  7643  peano5  7905  peano5OLD  7906  dmfexALT  7921  frpoins3xp3g  8155  fvmpocurryd  8286  qliftfuns  8833  nneneq  9243  nneneqOLD  9255  ttrcltr  9759  ttrclselem2  9769  frins3  9798  cfslb  10309  hsmexlem4  10472  axdc3lem2  10494  axdc4lem  10498  adderpq  10999  mulerpq  11000  ltordlem  11789  lble  12218  uz11  12899  xrsupsslem  13340  xrinfmsslem  13341  xrsupss  13342  xrinfmss  13343  fseqsupubi  13998  hashbclem  14469  ccatass  14596  swrdswrd  14713  swrdccatin1  14733  swrdccatin2  14737  cshwcsh2id  14837  wwlktovf  14965  isercolllem1  15669  caucvgb  15684  zsum  15722  fsum  15724  fsumf1o  15727  fsumcvg2  15731  isummulc2  15766  fsum2dlem  15774  fsumcom2  15778  fsumshftm  15785  fsum0diag2  15787  fsum00  15802  fsumrlim  15815  o1fsum  15817  isumshft  15843  clim2prod  15892  ntrivcvgfvn0  15903  zprod  15939  fprod  15943  fprodf1o  15948  prodss  15949  fprodser  15951  fprodcllemf  15960  fprodm1s  15972  fprodp1s  15973  fprodabs  15976  fprod2dlem  15982  fprodcom2  15986  fprodefsum  16097  mod2eq1n2dvds  16349  sumeven  16389  lcmfun  16646  pythagtriplem4  16821  pcmptdvds  16896  prslem  18323  posi  18342  dlatmjdi  18548  lidrididd  18663  grpidinv2  18992  ghmlin  19215  cntzmhm2  19336  dprdss  20029  dprd2d2  20044  srgrz  20190  srglz  20191  ringinvnz1ne0  20279  rrgeq0i  20677  lmodlema  20841  islmodd  20842  lsscl  20919  lsslss  20938  lspdisjb  21107  lsslinds  21829  assalem  21855  fvmptnn04if  22842  chfacfscmulgsum  22853  chfacfpmmulgsum  22857  ssnei2  23111  t1ficld  23322  t1sep2  23364  unconn  23424  1stcclb  23439  ptbasfi  23576  tx1stc  23645  qtoptop2  23694  r0sep  23743  ustincl  24203  ustdiag  24204  ustinvel  24205  ustexhalf  24206  psmet0  24305  psmettri2  24306  prdsdsf  24364  prdsxmet  24366  cncfi  24905  ovolfiniun  25521  mbfimaopnlem  25675  limciun  25914  dvcn  25942  dvmptfsum  25998  dvfsumle  26045  dvfsumleOLD  26046  dvfsumabs  26048  dvfsumlem3  26054  itgsubst  26075  fsumvma  27242  dchrelbasd  27268  dchrisumlem3  27520  sssslt1  27825  sssslt2  27826  madeval2  27877  elmade  27891  axcontlem9  28906  usgruspgrb  29119  uspgrloopvtxel  29453  umgr2v2evtxel  29459  clwwlknonex2lem2  30041  3spthd  30109  grpoass  30436  lnolin  30687  elnlfn  31861  strlem4  32187  hstrlem4  32195  atmd  32332  nn0min  32721  omndadd  32941  slmdlema  33067  qsxpid  33237  esumcvg  33919  measxun2  34043  sibfima  34172  bnj110  34703  bnj594  34757  bnj1491  34902  loop1cycl  34965  cvmcov  35091  mrsubcn  35347  dfon2lem5  35611  ifscgr  35868  nn0prpw  36035  neibastop2lem  36072  bj-restb  36801  poimirlem25  37346  poimirlem32  37353  mbfresfi  37367  totbndss  37478  ghomlinOLD  37589  rngodi  37605  rngodir  37606  rngoass  37607  rngohomadd  37670  rngohommul  37671  crngocom  37702  idladdcl  37720  idllmulcl  37721  idlrmulcl  37722  exlimddvf  37822  oposlem  38880  cvlexch1  39026  hlsuprexch  39080  lautle  39783  elrfirn2  42353  wepwsolem  42703  kelac1  42724  islssfg2  42732  lnmlssfg  42741  onov0suclim  42940  ovolval5lem3  46275  2elfz3nn0  46929  2elfz2melfz  46931  icceuelpartlem  47007  wtgoldbnnsum4prm  47374  bgoldbnnsum3prm  47376  bgoldbtbnd  47381  setrec2fun  48438

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »