Theorem syldan 282

Description: A syllogism deduction with conjoined antecents. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 6-Apr-2013.)

Hypotheses

Ref	Expression
syldan.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
syldan.2	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
syldan	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem syldan

Step	Hyp	Ref	Expression
1		syldan.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2		syldan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
3	2	expcom 116	. . 3 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	adantrd 279	. 2 ⊢ (𝜒 → ((𝜑 ∧ 𝜓) → 𝜃))
5	1, 4	mpcom 36	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108

This theorem is used by:  sylan2  286  dn1dc  973  stoic2a  1478  sbcied2  3089  csbied2  3195  elpw2g  4294  pofun  4459  tfi  4731  fnbr  5488  caovlem2d  6285  caofcom  6337  fnexALT  6344  elabreximd  6360  tfr1onlemres  6625  tfrcllemres  6638  tfri3  6643  ixpexgg  7010  f1domg  7050  fundmfi  7257  f1ofi  7263  finacn  7567  archnqq  7791  nqpru  7926  ltaddpr  7971  1idsr  8142  addgt0sr  8149  suplocsrlempr  8181  gt0ap0  8963  ap0gt0  8977  mulgt1  9202  gt0div  9209  ge0div  9210  ltdiv2  9226  creur  9298  avgle1  9558  recnz  9750  qreccl  10058  xrrege0  10244  peano2fzor  10667  flqltnz  10743  flqdiv  10779  zmodcl  10802  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  seqfveqg  10936  seq3fveq  10937  ser3mono  10945  seqsplitg  10947  seqcaopr2g  10952  iseqf1olemkle  10955  seq3f1olemqsumkj  10969  seq3f1olemqsumk  10970  seqf1oglem2  10978  seqf1og  10979  seq3id  10983  seq3z  10986  seqhomog  10988  le2sq2  11073  bcpasc  11226  fihasheqf1oi  11248  seq3coll  11316  wrdnval  11357  wrdsymb1  11363  lswcl  11377  ccatlid  11396  ccatass  11398  ccat1st1st  11431  lswccats1fst  11434  swrdlsw  11463  ccatswrd  11464  pfxtrcfvl  11491  pfxsuff1eqwrdeq  11493  ccatpfx  11495  pfx1  11497  pfxswrd  11500  pfxlswccat  11507  swrdccatin2  11523  pfxccatin12  11527  caucvgrelemcau  11768  caucvgre  11769  r19.2uz  11781  sqrtgt0  11822  xrmaxiflemval  12041  clim2ser  12128  clim2ser2  12129  climub  12135  serf0  12143  fsumf1o  12182  fisumss  12184  fsumcl2lem  12190  fsumsplit  12199  fsum2dlemstep  12226  fisumrev2  12238  fsumlessfi  12252  telfsumo  12258  fsumparts  12262  fsumiun  12269  binom1dif  12279  isumsplit  12283  isumrpcl  12286  isumlessdc  12288  explecnv  12297  cvgratnnlemmn  12317  cvgratz  12324  cvgratgt0  12325  mertenslemi1  12327  clim2prod  12331  clim2divap  12332  fprodseq  12375  fprodf1o  12380  prodssdc  12381  fprodssdc  12382  fprodsplitdc  12388  fprodeq0  12409  fprod2dlemstep  12414  ef0lem  12452  eftlub  12482  tanval3ap  12506  dvdssubr  12631  divalgmod  12719  bitsdc  12739  bitsp1  12743  divgcdnn  12777  algfx  12855  eucalgcvga  12861  lcmcllem  12870  lcmneg  12877  isprm6  12951  cncongrprm  12961  nn0sqdcq  13013  phimullem  13032  pcid  13132  pcgcd  13137  pcz  13140  4sqlem9  13194  4sqlem15  13213  4sqlem16  13214  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemsel1i  13314  ballotfilemsima  13317  ballotfilemfrceq  13330  imasex  13685  grpidd  13762  gzsumress  13771  ismndd  13809  subsubm  13849  grpinvid1  13916  grpinvid2  13917  grplcan  13926  grpinvinv  13931  grpinvval2  13947  mulgass  14021  mulgpropdg  14026  subginv  14043  subgmulg  14050  issubg2m  14051  issubg4m  14055  subsubg  14059  eqger  14086  qusinv  14098  resghm  14122  conjsubgen  14140  gsum2dfilem2  14272  rngrz  14352  isrngd  14359  ringidss  14441  isringd  14453  ringlz  14455  ringrz  14456  unitgrp  14532  0unit  14545  unitnegcl  14546  dvrass  14555  dvreq1  14558  dvrdir  14559  ringinvdv  14561  invrpropdg  14565  rhmunitinv  14594  issubrng2  14627  subsubrng  14631  subrg1  14648  issubrg2  14658  subsubrg  14662  lmod0vs  14767  lmodvs0  14768  lmodvneg1  14776  islss3  14825  lspsnsubg  14842  lspid  14843  lspssv  14844  lspidm  14847  lspsnneg  14866  sraval  14883  qus1  14972  zringmulg  15042  mulgrhm  15053  znidom  15101  issubassa3  15121  psrass1filem  15196  psrlidmfi  15219  tgcl  15323  tgclb  15324  tgss2  15338  ntrss3  15382  ntridm  15385  opnssneib  15415  ssnei2  15416  innei  15422  resttopon  15430  cnpnei  15478  cnntri  15483  lmss  15505  txcnp  15530  blpnfctr  15698  mopni2  15742  bdmopn  15763  climcncf  15843  ivthdec  15903  cnplimcim  15926  dvconst  15953  dvconstre  15955  dvef  15986  plymullem  16009  plycoeid3  16016  rpcxpneg  16173  abscxp  16183  log2tlbndlog2  16253  birthdaylem2  16259  ppiqsval  16273  ppiprm  16292  chtprm  16294  chtdif  16297  ppiqltx  16314  prmorcht  16315  sgmmul  16323  chtqleppi  16327  chtublem  16328  bposlem3  16346  lgscllem  16364  lgsvalmod  16376  lgsdir2  16390  lgsquadlem2  16435  lgsquad2lem2  16439  upgredg  16623  usgruspgrben  16665  usgredg3  16693  cvgcmp2nlemabs  17320  trilpolemisumle  17327  trilpolemeq1  17329  trilpolemlt1  17330  nconstwlpolemgt0  17354  neapmkvlem  17357