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  904  stoic2a  1361  sbcied2  2865  csbied2  2964  elpw2g  3967  pofun  4113  tfi  4370  fnbr  5081  caovlem2d  5794  grprinvlem  5796  caofcom  5835  fnexALT  5841  tfr1onlemres  6068  tfrcllemres  6081  tfri3  6086  f1domg  6427  fundmfi  6597  f1ofi  6602  archnqq  6920  nqpru  7055  ltaddpr  7100  1idsr  7258  addgt0sr  7265  gt0ap0  8043  ap0gt0  8056  mulgt1  8259  gt0div  8266  ge0div  8267  ltdiv2  8283  creur  8354  avgle1  8589  recnz  8772  qreccl  9059  xrrege0  9219  peano2fzor  9571  flqltnz  9622  flqdiv  9656  zmodcl  9679  frecuzrdgtcl  9747  frecuzrdgfunlem  9754  iseqfveq  9804  isermono  9811  iseqsplit  9812  iseqf1olemkle  9817  iseqf1olemqsumkj  9831  iseqf1olemqsumk  9832  iseqid  9842  iseqz  9845  le2sq2  9928  bcpasc  10070  fihasheqf1oi  10092  iseqcoll  10143  caucvgrelemcau  10308  caucvgre  10309  r19.2uz  10321  sqrtgt0  10362  clim2iser  10617  clim2iser2  10618  climub  10624  serif0  10631  fsumf1o  10668  fisumss  10670  dvdssubr  10717  divalgmod  10802  divgcdnn  10841  ialgfx  10909  eucialgcvga  10915  lcmcllem  10924  lcmneg  10931  isprm6  11001  cncongrprm  11011  phimullem  11076