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  902  stoic2a  1359  sbcied2  2862  csbied2  2960  elpw2g  3957  pofun  4103  tfi  4360  fnbr  5069  caovlem2d  5772  grprinvlem  5774  caofcom  5813  fnexALT  5819  tfr1onlemres  6046  tfrcllemres  6059  tfri3  6064  f1domg  6405  fundmfi  6572  f1ofi  6577  archnqq  6879  nqpru  7014  ltaddpr  7059  1idsr  7217  addgt0sr  7224  gt0ap0  8002  ap0gt0  8015  mulgt1  8218  gt0div  8225  ge0div  8226  ltdiv2  8242  creur  8313  avgle1  8548  recnz  8735  qreccl  9022  xrrege0  9182  peano2fzor  9532  flqltnz  9583  flqdiv  9617  zmodcl  9640  frecuzrdgtcl  9708  frecuzrdgfunlem  9715  iseqfveq  9765  isermono  9772  iseqsplit  9773  iseqid  9782  iseqz  9785  le2sq2  9867  bcpasc  10009  fihasheqf1oi  10031  caucvgrelemcau  10240  caucvgre  10241  r19.2uz  10253  sqrtgt0  10294  clim2iser  10549  clim2iser2  10550  climub  10556  serif0  10563  dvdssubr  10622  divalgmod  10707  divgcdnn  10746  ialgfx  10814  eucialgcvga  10820  lcmcllem  10829  lcmneg  10836  isprm6  10906  cncongrprm  10916  phimullem  10981