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  966  stoic2a  1471  sbcied2  3066  csbied2  3172  elpw2g  4241  pofun  4404  tfi  4675  fnbr  5428  caovlem2d  6207  caofcom  6258  fnexALT  6265  tfr1onlemres  6506  tfrcllemres  6519  tfri3  6524  ixpexgg  6882  f1domg  6922  fundmfi  7120  f1ofi  7126  finacn  7402  archnqq  7620  nqpru  7755  ltaddpr  7800  1idsr  7971  addgt0sr  7978  suplocsrlempr  8010  gt0ap0  8789  ap0gt0  8803  mulgt1  9026  gt0div  9033  ge0div  9034  ltdiv2  9050  creur  9122  avgle1  9368  recnz  9556  qreccl  9854  xrrege0  10038  peano2fzor  10455  flqltnz  10524  flqdiv  10560  zmodcl  10583  frecuzrdgtcl  10651  frecuzrdgfunlem  10658  seqfveqg  10717  seq3fveq  10718  ser3mono  10726  seqsplitg  10728  seqcaopr2g  10733  iseqf1olemkle  10736  seq3f1olemqsumkj  10750  seq3f1olemqsumk  10751  seqf1oglem2  10759  seqf1og  10760  seq3id  10764  seq3z  10767  seqhomog  10769  le2sq2  10854  bcpasc  11005  fihasheqf1oi  11026  seq3coll  11082  wrdnval  11120  wrdsymb1  11126  lswcl  11140  ccatlid  11159  ccatass  11161  ccat1st1st  11193  lswccats1fst  11196  swrdlsw  11222  ccatswrd  11223  pfxtrcfvl  11250  pfxsuff1eqwrdeq  11252  ccatpfx  11254  pfx1  11256  pfxswrd  11259  pfxlswccat  11266  swrdccatin2  11282  pfxccatin12  11286  caucvgrelemcau  11512  caucvgre  11513  r19.2uz  11525  sqrtgt0  11566  xrmaxiflemval  11782  clim2ser  11869  clim2ser2  11870  climub  11876  serf0  11884  fsumf1o  11922  fisumss  11924  fsumcl2lem  11930  fsumsplit  11939  fsum2dlemstep  11966  fisumrev2  11978  fsumlessfi  11992  telfsumo  11998  fsumparts  12002  fsumiun  12009  binom1dif  12019  isumsplit  12023  isumrpcl  12026  isumlessdc  12028  explecnv  12037  cvgratnnlemmn  12057  cvgratz  12064  cvgratgt0  12065  mertenslemi1  12067  clim2prod  12071  clim2divap  12072  fprodseq  12115  fprodf1o  12120  prodssdc  12121  fprodssdc  12122  fprodsplitdc  12128  fprodeq0  12149  fprod2dlemstep  12154  ef0lem  12192  eftlub  12222  tanval3ap  12246  dvdssubr  12371  divalgmod  12459  bitsdc  12479  bitsp1  12483  divgcdnn  12517  algfx  12595  eucalgcvga  12601  lcmcllem  12610  lcmneg  12617  isprm6  12690  cncongrprm  12700  phimullem  12768  pcid  12868  pcgcd  12873  pcz  12876  4sqlem9  12930  4sqlem15  12949  4sqlem16  12950  imasex  13359  grpidd  13437  gsumress  13449  ismndd  13491  subsubm  13537  grpinvid1  13606  grpinvid2  13607  grplcan  13616  grpinvinv  13621  grpinvval2  13637  mulgass  13717  mulgpropdg  13722  subginv  13739  subgmulg  13746  issubg2m  13747  issubg4m  13751  subsubg  13755  eqger  13782  qusinv  13794  resghm  13818  conjsubgen  13836  rngrz  13930  isrngd  13937  ringidss  14013  isringd  14025  ringlz  14027  ringrz  14028  unitgrp  14101  0unit  14114  unitnegcl  14115  dvrass  14124  dvreq1  14127  dvrdir  14128  ringinvdv  14130  invrpropdg  14134  rhmunitinv  14163  issubrng2  14195  subsubrng  14199  subrg1  14216  issubrg2  14226  subsubrg  14230  lmod0vs  14306  lmodvs0  14307  lmodvneg1  14315  islss3  14364  lspsnsubg  14381  lspid  14382  lspssv  14383  lspidm  14386  lspsnneg  14405  sraval  14422  qus1  14511  zringmulg  14583  mulgrhm  14594  znidom  14642  tgcl  14759  tgclb  14760  tgss2  14774  ntrss3  14818  ntridm  14821  opnssneib  14851  ssnei2  14852  innei  14858  resttopon  14866  cnpnei  14914  cnntri  14919  lmss  14941  txcnp  14966  blpnfctr  15134  mopni2  15178  bdmopn  15199  climcncf  15279  ivthdec  15339  cnplimcim  15362  dvconst  15389  dvconstre  15391  dvef  15422  plymullem  15445  plycoeid3  15452  rpcxpneg  15602  abscxp  15610  sgmmul  15691  lgscllem  15707  lgsvalmod  15719  lgsdir2  15733  lgsquadlem2  15778  lgsquad2lem2  15782  upgredg  15963  usgruspgrben  16005  usgredg3  16033  cvgcmp2nlemabs  16514  trilpolemisumle  16520  trilpolemeq1  16522  trilpolemlt1  16523  nconstwlpolemgt0  16546  neapmkvlem  16549