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 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108

This theorem is referenced by:  sylan2  286  dn1dc  969  stoic2a  1474  sbcied2  3070  csbied2  3176  elpw2g  4251  pofun  4415  tfi  4686  fnbr  5441  caovlem2d  6225  caofcom  6275  fnexALT  6282  tfr1onlemres  6558  tfrcllemres  6571  tfri3  6576  ixpexgg  6934  f1domg  6974  fundmfi  7179  f1ofi  7185  finacn  7462  archnqq  7680  nqpru  7815  ltaddpr  7860  1idsr  8031  addgt0sr  8038  suplocsrlempr  8070  gt0ap0  8849  ap0gt0  8863  mulgt1  9086  gt0div  9093  ge0div  9094  ltdiv2  9110  creur  9182  avgle1  9428  recnz  9616  qreccl  9919  xrrege0  10103  peano2fzor  10521  flqltnz  10591  flqdiv  10627  zmodcl  10650  frecuzrdgtcl  10718  frecuzrdgfunlem  10725  seqfveqg  10784  seq3fveq  10785  ser3mono  10793  seqsplitg  10795  seqcaopr2g  10800  iseqf1olemkle  10803  seq3f1olemqsumkj  10817  seq3f1olemqsumk  10818  seqf1oglem2  10826  seqf1og  10827  seq3id  10831  seq3z  10834  seqhomog  10836  le2sq2  10921  bcpasc  11072  fihasheqf1oi  11093  seq3coll  11150  wrdnval  11191  wrdsymb1  11197  lswcl  11211  ccatlid  11230  ccatass  11232  ccat1st1st  11265  lswccats1fst  11268  swrdlsw  11297  ccatswrd  11298  pfxtrcfvl  11325  pfxsuff1eqwrdeq  11327  ccatpfx  11329  pfx1  11331  pfxswrd  11334  pfxlswccat  11341  swrdccatin2  11357  pfxccatin12  11361  caucvgrelemcau  11601  caucvgre  11602  r19.2uz  11614  sqrtgt0  11655  xrmaxiflemval  11871  clim2ser  11958  clim2ser2  11959  climub  11965  serf0  11973  fsumf1o  12012  fisumss  12014  fsumcl2lem  12020  fsumsplit  12029  fsum2dlemstep  12056  fisumrev2  12068  fsumlessfi  12082  telfsumo  12088  fsumparts  12092  fsumiun  12099  binom1dif  12109  isumsplit  12113  isumrpcl  12116  isumlessdc  12118  explecnv  12127  cvgratnnlemmn  12147  cvgratz  12154  cvgratgt0  12155  mertenslemi1  12157  clim2prod  12161  clim2divap  12162  fprodseq  12205  fprodf1o  12210  prodssdc  12211  fprodssdc  12212  fprodsplitdc  12218  fprodeq0  12239  fprod2dlemstep  12244  ef0lem  12282  eftlub  12312  tanval3ap  12336  dvdssubr  12461  divalgmod  12549  bitsdc  12569  bitsp1  12573  divgcdnn  12607  algfx  12685  eucalgcvga  12691  lcmcllem  12700  lcmneg  12707  isprm6  12780  cncongrprm  12790  phimullem  12858  pcid  12958  pcgcd  12963  pcz  12966  4sqlem9  13020  4sqlem15  13039  4sqlem16  13040  imasex  13449  grpidd  13527  gsumress  13539  ismndd  13581  subsubm  13627  grpinvid1  13696  grpinvid2  13697  grplcan  13706  grpinvinv  13711  grpinvval2  13727  mulgass  13807  mulgpropdg  13812  subginv  13829  subgmulg  13836  issubg2m  13837  issubg4m  13841  subsubg  13845  eqger  13872  qusinv  13884  resghm  13908  conjsubgen  13926  rngrz  14021  isrngd  14028  ringidss  14104  isringd  14116  ringlz  14118  ringrz  14119  unitgrp  14192  0unit  14205  unitnegcl  14206  dvrass  14215  dvreq1  14218  dvrdir  14219  ringinvdv  14221  invrpropdg  14225  rhmunitinv  14254  issubrng2  14286  subsubrng  14290  subrg1  14307  issubrg2  14317  subsubrg  14321  lmod0vs  14397  lmodvs0  14398  lmodvneg1  14406  islss3  14455  lspsnsubg  14472  lspid  14473  lspssv  14474  lspidm  14477  lspsnneg  14496  sraval  14513  qus1  14602  zringmulg  14674  mulgrhm  14685  znidom  14733  tgcl  14855  tgclb  14856  tgss2  14870  ntrss3  14914  ntridm  14917  opnssneib  14947  ssnei2  14948  innei  14954  resttopon  14962  cnpnei  15010  cnntri  15015  lmss  15037  txcnp  15062  blpnfctr  15230  mopni2  15274  bdmopn  15295  climcncf  15375  ivthdec  15435  cnplimcim  15458  dvconst  15485  dvconstre  15487  dvef  15518  plymullem  15541  plycoeid3  15548  rpcxpneg  15698  abscxp  15706  sgmmul  15790  lgscllem  15806  lgsvalmod  15818  lgsdir2  15832  lgsquadlem2  15877  lgsquad2lem2  15881  upgredg  16065  usgruspgrben  16107  usgredg3  16135  cvgcmp2nlemabs  16744  trilpolemisumle  16750  trilpolemeq1  16752  trilpolemlt1  16753  nconstwlpolemgt0  16777  neapmkvlem  16780