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  4292  pofun  4457  tfi  4729  fnbr  5485  caovlem2d  6282  caofcom  6333  fnexALT  6340  elabreximd  6356  tfr1onlemres  6620  tfrcllemres  6633  tfri3  6638  ixpexgg  7004  f1domg  7044  fundmfi  7251  f1ofi  7257  finacn  7561  archnqq  7785  nqpru  7920  ltaddpr  7965  1idsr  8136  addgt0sr  8143  suplocsrlempr  8175  gt0ap0  8957  ap0gt0  8971  mulgt1  9196  gt0div  9203  ge0div  9204  ltdiv2  9220  creur  9292  avgle1  9551  recnz  9744  qreccl  10052  xrrege0  10238  peano2fzor  10661  flqltnz  10736  flqdiv  10772  zmodcl  10795  frecuzrdgtcl  10863  frecuzrdgfunlem  10870  seqfveqg  10929  seq3fveq  10930  ser3mono  10938  seqsplitg  10940  seqcaopr2g  10945  iseqf1olemkle  10948  seq3f1olemqsumkj  10962  seq3f1olemqsumk  10963  seqf1oglem2  10971  seqf1og  10972  seq3id  10976  seq3z  10979  seqhomog  10981  le2sq2  11066  bcpasc  11219  fihasheqf1oi  11241  seq3coll  11309  wrdnval  11350  wrdsymb1  11356  lswcl  11370  ccatlid  11389  ccatass  11391  ccat1st1st  11424  lswccats1fst  11427  swrdlsw  11456  ccatswrd  11457  pfxtrcfvl  11484  pfxsuff1eqwrdeq  11486  ccatpfx  11488  pfx1  11490  pfxswrd  11493  pfxlswccat  11500  swrdccatin2  11516  pfxccatin12  11520  caucvgrelemcau  11761  caucvgre  11762  r19.2uz  11774  sqrtgt0  11815  xrmaxiflemval  12034  clim2ser  12121  clim2ser2  12122  climub  12128  serf0  12136  fsumf1o  12175  fisumss  12177  fsumcl2lem  12183  fsumsplit  12192  fsum2dlemstep  12219  fisumrev2  12231  fsumlessfi  12245  telfsumo  12251  fsumparts  12255  fsumiun  12262  binom1dif  12272  isumsplit  12276  isumrpcl  12279  isumlessdc  12281  explecnv  12290  cvgratnnlemmn  12310  cvgratz  12317  cvgratgt0  12318  mertenslemi1  12320  clim2prod  12324  clim2divap  12325  fprodseq  12368  fprodf1o  12373  prodssdc  12374  fprodssdc  12375  fprodsplitdc  12381  fprodeq0  12402  fprod2dlemstep  12407  ef0lem  12445  eftlub  12475  tanval3ap  12499  dvdssubr  12624  divalgmod  12712  bitsdc  12732  bitsp1  12736  divgcdnn  12770  algfx  12848  eucalgcvga  12854  lcmcllem  12863  lcmneg  12870  isprm6  12944  cncongrprm  12954  nn0sqdcq  13006  phimullem  13025  pcid  13125  pcgcd  13130  pcz  13133  4sqlem9  13187  4sqlem15  13206  4sqlem16  13207  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemsel1i  13307  ballotfilemsima  13310  ballotfilemfrceq  13323  imasex  13677  grpidd  13754  gzsumress  13763  ismndd  13801  subsubm  13841  grpinvid1  13908  grpinvid2  13909  grplcan  13918  grpinvinv  13923  grpinvval2  13939  mulgass  14013  mulgpropdg  14018  subginv  14035  subgmulg  14042  issubg2m  14043  issubg4m  14047  subsubg  14051  eqger  14078  qusinv  14090  resghm  14114  conjsubgen  14132  rngrz  14296  isrngd  14303  ringidss  14385  isringd  14397  ringlz  14399  ringrz  14400  unitgrp  14474  0unit  14487  unitnegcl  14488  dvrass  14497  dvreq1  14500  dvrdir  14501  ringinvdv  14503  invrpropdg  14507  rhmunitinv  14536  issubrng2  14569  subsubrng  14573  subrg1  14590  issubrg2  14600  subsubrg  14604  lmod0vs  14709  lmodvs0  14710  lmodvneg1  14718  islss3  14767  lspsnsubg  14784  lspid  14785  lspssv  14786  lspidm  14789  lspsnneg  14808  sraval  14825  qus1  14914  zringmulg  14984  mulgrhm  14995  znidom  15043  issubassa3  15063  tgcl  15217  tgclb  15218  tgss2  15232  ntrss3  15276  ntridm  15279  opnssneib  15309  ssnei2  15310  innei  15316  resttopon  15324  cnpnei  15372  cnntri  15377  lmss  15399  txcnp  15424  blpnfctr  15592  mopni2  15636  bdmopn  15657  climcncf  15737  ivthdec  15797  cnplimcim  15820  dvconst  15847  dvconstre  15849  dvef  15880  plymullem  15903  plycoeid3  15910  rpcxpneg  16065  abscxp  16073  log2tlbndlog2  16142  birthdaylem2  16148  ppiqsval  16162  ppiprm  16181  chtprm  16183  chtdif  16186  ppiqltx  16203  prmorcht  16204  sgmmul  16212  chtqleppi  16216  chtublem  16217  bposlem3  16235  lgscllem  16248  lgsvalmod  16260  lgsdir2  16274  lgsquadlem2  16319  lgsquad2lem2  16323  upgredg  16507  usgruspgrben  16549  usgredg3  16577  cvgcmp2nlemabs  17203  trilpolemisumle  17209  trilpolemeq1  17211  trilpolemlt1  17212  nconstwlpolemgt0  17236  neapmkvlem  17239