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  968  stoic2a  1473  sbcied2  3069  csbied2  3175  elpw2g  4246  pofun  4409  tfi  4680  fnbr  5434  caovlem2d  6215  caofcom  6266  fnexALT  6273  tfr1onlemres  6515  tfrcllemres  6528  tfri3  6533  ixpexgg  6891  f1domg  6931  fundmfi  7136  f1ofi  7142  finacn  7419  archnqq  7637  nqpru  7772  ltaddpr  7817  1idsr  7988  addgt0sr  7995  suplocsrlempr  8027  gt0ap0  8806  ap0gt0  8820  mulgt1  9043  gt0div  9050  ge0div  9051  ltdiv2  9067  creur  9139  avgle1  9385  recnz  9573  qreccl  9876  xrrege0  10060  peano2fzor  10478  flqltnz  10548  flqdiv  10584  zmodcl  10607  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  seqfveqg  10741  seq3fveq  10742  ser3mono  10750  seqsplitg  10752  seqcaopr2g  10757  iseqf1olemkle  10760  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seqf1oglem2  10783  seqf1og  10784  seq3id  10788  seq3z  10791  seqhomog  10793  le2sq2  10878  bcpasc  11029  fihasheqf1oi  11050  seq3coll  11107  wrdnval  11148  wrdsymb1  11154  lswcl  11168  ccatlid  11187  ccatass  11189  ccat1st1st  11222  lswccats1fst  11225  swrdlsw  11254  ccatswrd  11255  pfxtrcfvl  11282  pfxsuff1eqwrdeq  11284  ccatpfx  11286  pfx1  11288  pfxswrd  11291  pfxlswccat  11298  swrdccatin2  11314  pfxccatin12  11318  caucvgrelemcau  11545  caucvgre  11546  r19.2uz  11558  sqrtgt0  11599  xrmaxiflemval  11815  clim2ser  11902  clim2ser2  11903  climub  11909  serf0  11917  fsumf1o  11956  fisumss  11958  fsumcl2lem  11964  fsumsplit  11973  fsum2dlemstep  12000  fisumrev2  12012  fsumlessfi  12026  telfsumo  12032  fsumparts  12036  fsumiun  12043  binom1dif  12053  isumsplit  12057  isumrpcl  12060  isumlessdc  12062  explecnv  12071  cvgratnnlemmn  12091  cvgratz  12098  cvgratgt0  12099  mertenslemi1  12101  clim2prod  12105  clim2divap  12106  fprodseq  12149  fprodf1o  12154  prodssdc  12155  fprodssdc  12156  fprodsplitdc  12162  fprodeq0  12183  fprod2dlemstep  12188  ef0lem  12226  eftlub  12256  tanval3ap  12280  dvdssubr  12405  divalgmod  12493  bitsdc  12513  bitsp1  12517  divgcdnn  12551  algfx  12629  eucalgcvga  12635  lcmcllem  12644  lcmneg  12651  isprm6  12724  cncongrprm  12734  phimullem  12802  pcid  12902  pcgcd  12907  pcz  12910  4sqlem9  12964  4sqlem15  12983  4sqlem16  12984  imasex  13393  grpidd  13471  gsumress  13483  ismndd  13525  subsubm  13571  grpinvid1  13640  grpinvid2  13641  grplcan  13650  grpinvinv  13655  grpinvval2  13671  mulgass  13751  mulgpropdg  13756  subginv  13773  subgmulg  13780  issubg2m  13781  issubg4m  13785  subsubg  13789  eqger  13816  qusinv  13828  resghm  13852  conjsubgen  13870  rngrz  13965  isrngd  13972  ringidss  14048  isringd  14060  ringlz  14062  ringrz  14063  unitgrp  14136  0unit  14149  unitnegcl  14150  dvrass  14159  dvreq1  14162  dvrdir  14163  ringinvdv  14165  invrpropdg  14169  rhmunitinv  14198  issubrng2  14230  subsubrng  14234  subrg1  14251  issubrg2  14261  subsubrg  14265  lmod0vs  14341  lmodvs0  14342  lmodvneg1  14350  islss3  14399  lspsnsubg  14416  lspid  14417  lspssv  14418  lspidm  14421  lspsnneg  14440  sraval  14457  qus1  14546  zringmulg  14618  mulgrhm  14629  znidom  14677  tgcl  14794  tgclb  14795  tgss2  14809  ntrss3  14853  ntridm  14856  opnssneib  14886  ssnei2  14887  innei  14893  resttopon  14901  cnpnei  14949  cnntri  14954  lmss  14976  txcnp  15001  blpnfctr  15169  mopni2  15213  bdmopn  15234  climcncf  15314  ivthdec  15374  cnplimcim  15397  dvconst  15424  dvconstre  15426  dvef  15457  plymullem  15480  plycoeid3  15487  rpcxpneg  15637  abscxp  15645  sgmmul  15726  lgscllem  15742  lgsvalmod  15754  lgsdir2  15768  lgsquadlem2  15813  lgsquad2lem2  15817  upgredg  16001  usgruspgrben  16043  usgredg3  16071  cvgcmp2nlemabs  16662  trilpolemisumle  16668  trilpolemeq1  16670  trilpolemlt1  16671  nconstwlpolemgt0  16694  neapmkvlem  16697