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  6624  tfrcllemres  6637  tfri3  6642  ixpexgg  7009  f1domg  7049  fundmfi  7256  f1ofi  7262  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  9751  qreccl  10059  xrrege0  10245  peano2fzor  10668  flqltnz  10744  flqdiv  10780  zmodcl  10803  frecuzrdgtcl  10871  frecuzrdgfunlem  10878  seqfveqg  10937  seq3fveq  10938  ser3mono  10946  seqsplitg  10948  seqcaopr2g  10953  iseqf1olemkle  10956  seq3f1olemqsumkj  10970  seq3f1olemqsumk  10971  seqf1oglem2  10979  seqf1og  10980  seq3id  10984  seq3z  10987  seqhomog  10989  le2sq2  11074  bcpasc  11227  fihasheqf1oi  11249  seq3coll  11317  wrdnval  11358  wrdsymb1  11364  lswcl  11378  ccatlid  11397  ccatass  11399  ccat1st1st  11432  lswccats1fst  11435  swrdlsw  11464  ccatswrd  11465  pfxtrcfvl  11492  pfxsuff1eqwrdeq  11494  ccatpfx  11496  pfx1  11498  pfxswrd  11501  pfxlswccat  11508  swrdccatin2  11524  pfxccatin12  11528  caucvgrelemcau  11769  caucvgre  11770  r19.2uz  11782  sqrtgt0  11823  xrmaxiflemval  12042  clim2ser  12129  clim2ser2  12130  climub  12136  serf0  12144  fsumf1o  12183  fisumss  12185  fsumcl2lem  12191  fsumsplit  12200  fsum2dlemstep  12227  fisumrev2  12239  fsumlessfi  12253  telfsumo  12259  fsumparts  12263  fsumiun  12270  binom1dif  12280  isumsplit  12284  isumrpcl  12287  isumlessdc  12289  explecnv  12298  cvgratnnlemmn  12318  cvgratz  12325  cvgratgt0  12326  mertenslemi1  12328  clim2prod  12332  clim2divap  12333  fprodseq  12376  fprodf1o  12381  prodssdc  12382  fprodssdc  12383  fprodsplitdc  12389  fprodeq0  12410  fprod2dlemstep  12415  ef0lem  12453  eftlub  12483  tanval3ap  12507  dvdssubr  12632  divalgmod  12720  bitsdc  12740  bitsp1  12744  divgcdnn  12778  algfx  12856  eucalgcvga  12862  lcmcllem  12871  lcmneg  12878  isprm6  12952  cncongrprm  12962  nn0sqdcq  13014  phimullem  13033  pcid  13133  pcgcd  13138  pcz  13141  4sqlem9  13195  4sqlem15  13214  4sqlem16  13215  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemsel1i  13315  ballotfilemsima  13318  ballotfilemfrceq  13331  imasex  13686  grpidd  13763  gzsumress  13772  ismndd  13810  subsubm  13850  grpinvid1  13917  grpinvid2  13918  grplcan  13927  grpinvinv  13932  grpinvval2  13948  mulgass  14022  mulgpropdg  14027  subginv  14044  subgmulg  14051  issubg2m  14052  issubg4m  14056  subsubg  14060  eqger  14087  qusinv  14099  resghm  14123  conjsubgen  14141  gsum2dfilem2  14273  rngrz  14353  isrngd  14360  ringidss  14442  isringd  14454  ringlz  14456  ringrz  14457  unitgrp  14533  0unit  14546  unitnegcl  14547  dvrass  14556  dvreq1  14559  dvrdir  14560  ringinvdv  14562  invrpropdg  14566  rhmunitinv  14595  issubrng2  14628  subsubrng  14632  subrg1  14649  issubrg2  14659  subsubrg  14663  lmod0vs  14768  lmodvs0  14769  lmodvneg1  14777  islss3  14826  lspsnsubg  14843  lspid  14844  lspssv  14845  lspidm  14848  lspsnneg  14867  sraval  14884  qus1  14973  zringmulg  15043  mulgrhm  15054  znidom  15102  issubassa3  15122  psrass1filem  15182  psrlidmfi  15204  tgcl  15302  tgclb  15303  tgss2  15317  ntrss3  15361  ntridm  15364  opnssneib  15394  ssnei2  15395  innei  15401  resttopon  15409  cnpnei  15457  cnntri  15462  lmss  15484  txcnp  15509  blpnfctr  15677  mopni2  15721  bdmopn  15742  climcncf  15822  ivthdec  15882  cnplimcim  15905  dvconst  15932  dvconstre  15934  dvef  15965  plymullem  15988  plycoeid3  15995  rpcxpneg  16152  abscxp  16162  log2tlbndlog2  16232  birthdaylem2  16238  ppiqsval  16252  ppiprm  16271  chtprm  16273  chtdif  16276  ppiqltx  16293  prmorcht  16294  sgmmul  16302  chtqleppi  16306  chtublem  16307  bposlem3  16325  lgscllem  16343  lgsvalmod  16355  lgsdir2  16369  lgsquadlem2  16414  lgsquad2lem2  16418  upgredg  16602  usgruspgrben  16644  usgredg3  16672  cvgcmp2nlemabs  17299  trilpolemisumle  17306  trilpolemeq1  17308  trilpolemlt1  17309  nconstwlpolemgt0  17333  neapmkvlem  17336