Theorem syldan 276

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  sylan2  280  dn1dc  901  stoic2a  1358  sbcied2  2851  csbied2  2949  elpw2g  3931  pofun  4067  tfi  4323  fnbr  5021  caovlem2d  5713  grprinvlem  5715  caofcom  5754  fnexALT  5760  tfri3  5976  f1domg  6261  fundmfi  6389  archnqq  6607  nqpru  6742  ltaddpr  6787  1idsr  6945  addgt0sr  6952  gt0ap0  7725  ap0gt0  7738  mulgt1  7941  gt0div  7948  ge0div  7949  ltdiv2  7965  creur  8036  avgle1  8271  recnz  8440  qreccl  8727  xrrege0  8892  peano2fzor  9241  flqltnz  9289  flqdiv  9323  zmodcl  9346  frecuzrdgfn  9414  frecuzrdgcl  9415  frecuzrdgsuc  9417  iseqfveq  9450  isermono  9457  iseqsplit  9458  iseqid  9467  iseqz  9469  le2sq2  9551  bcpasc  9693  caucvgrelemcau  9866  caucvgre  9867  r19.2uz  9879  sqrtgt0  9920  clim2iser  10175  clim2iser2  10176  climub  10182  serif0  10189  dvdssubr  10241  divalgmod  10327  divgcdnn  10366  ialgfx  10434  eucialgcvga  10440  lcmcllem  10449  lcmneg  10456  isprm6  10526  cncongrprm  10536