Theorem syldan 280

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 115	. . 3 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	adantrd 277	. 2 ⊢ (𝜒 → ((𝜑 ∧ 𝜓) → 𝜃))
5	1, 4	mpcom 36	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  sylan2  284  dn1dc  955  stoic2a  1422  sbcied2  2992  csbied2  3096  elpw2g  4140  pofun  4295  tfi  4564  fnbr  5298  caovlem2d  6042  caofcom  6081  fnexALT  6087  tfr1onlemres  6325  tfrcllemres  6338  tfri3  6343  ixpexgg  6696  f1domg  6732  fundmfi  6911  f1ofi  6916  archnqq  7366  nqpru  7501  ltaddpr  7546  1idsr  7717  addgt0sr  7724  suplocsrlempr  7756  gt0ap0  8532  ap0gt0  8546  mulgt1  8766  gt0div  8773  ge0div  8774  ltdiv2  8790  creur  8862  avgle1  9105  recnz  9292  qreccl  9588  xrrege0  9769  peano2fzor  10175  flqltnz  10230  flqdiv  10264  zmodcl  10287  frecuzrdgtcl  10355  frecuzrdgfunlem  10362  seq3fveq  10414  ser3mono  10421  iseqf1olemkle  10427  seq3f1olemqsumkj  10441  seq3f1olemqsumk  10442  seq3id  10451  seq3z  10454  le2sq2  10538  bcpasc  10687  fihasheqf1oi  10709  seq3coll  10764  caucvgrelemcau  10931  caucvgre  10932  r19.2uz  10944  sqrtgt0  10985  xrmaxiflemval  11200  clim2ser  11287  clim2ser2  11288  climub  11294  serf0  11302  fsumf1o  11340  fisumss  11342  fsumcl2lem  11348  fsumsplit  11357  fsum2dlemstep  11384  fisumrev2  11396  fsumlessfi  11410  telfsumo  11416  fsumparts  11420  fsumiun  11427  binom1dif  11437  isumsplit  11441  isumrpcl  11444  isumlessdc  11446  explecnv  11455  cvgratnnlemmn  11475  cvgratz  11482  cvgratgt0  11483  mertenslemi1  11485  clim2prod  11489  clim2divap  11490  fprodseq  11533  fprodf1o  11538  prodssdc  11539  fprodssdc  11540  fprodsplitdc  11546  fprodeq0  11567  fprod2dlemstep  11572  ef0lem  11610  eftlub  11640  tanval3ap  11664  dvdssubr  11788  divalgmod  11873  divgcdnn  11917  algfx  11993  eucalgcvga  11999  lcmcllem  12008  lcmneg  12015  isprm6  12088  cncongrprm  12098  phimullem  12166  pcid  12264  pcgcd  12269  pcz  12272  4sqlem9  12325  grpidd  12624  ismndd  12660  tgcl  12817  tgclb  12818  tgss2  12832  ntrss3  12876  ntridm  12879  opnssneib  12909  ssnei2  12910  innei  12916  resttopon  12924  cnpnei  12972  cnntri  12977  lmss  12999  txcnp  13024  blpnfctr  13192  mopni2  13236  bdmopn  13257  climcncf  13324  ivthdec  13375  cnplimcim  13389  dvconst  13414  dvef  13441  rpcxpneg  13581  abscxp  13588  lgscllem  13661  lgsvalmod  13673  lgsdir2  13687  cvgcmp2nlemabs  14024  trilpolemisumle  14030  trilpolemeq1  14032  trilpolemlt1  14033  nconstwlpolemgt0  14055  neapmkvlem  14058