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  944  stoic2a  1405  sbcied2  2941  csbied2  3042  elpw2g  4076  pofun  4229  tfi  4491  fnbr  5220  caovlem2d  5956  grprinvlem  5958  caofcom  5998  fnexALT  6004  tfr1onlemres  6239  tfrcllemres  6252  tfri3  6257  ixpexgg  6609  f1domg  6645  fundmfi  6819  f1ofi  6824  archnqq  7218  nqpru  7353  ltaddpr  7398  1idsr  7569  addgt0sr  7576  suplocsrlempr  7608  gt0ap0  8381  ap0gt0  8395  mulgt1  8614  gt0div  8621  ge0div  8622  ltdiv2  8638  creur  8710  avgle1  8953  recnz  9137  qreccl  9427  xrrege0  9601  peano2fzor  10002  flqltnz  10053  flqdiv  10087  zmodcl  10110  frecuzrdgtcl  10178  frecuzrdgfunlem  10185  seq3fveq  10237  ser3mono  10244  iseqf1olemkle  10250  seq3f1olemqsumkj  10264  seq3f1olemqsumk  10265  seq3id  10274  seq3z  10277  le2sq2  10361  bcpasc  10505  fihasheqf1oi  10527  seq3coll  10578  caucvgrelemcau  10745  caucvgre  10746  r19.2uz  10758  sqrtgt0  10799  xrmaxiflemval  11012  clim2ser  11099  clim2ser2  11100  climub  11106  serf0  11114  fsumf1o  11152  fisumss  11154  fsumcl2lem  11160  fsumsplit  11169  fsum2dlemstep  11196  fisumrev2  11208  fsumlessfi  11222  telfsumo  11228  fsumparts  11232  fsumiun  11239  binom1dif  11249  isumsplit  11253  isumrpcl  11256  isumlessdc  11258  explecnv  11267  cvgratnnlemmn  11287  cvgratz  11294  cvgratgt0  11295  mertenslemi1  11297  clim2prod  11301  clim2divap  11302  ef0lem  11355  eftlub  11385  tanval3ap  11410  dvdssubr  11528  divalgmod  11613  divgcdnn  11652  algfx  11722  eucalgcvga  11728  lcmcllem  11737  lcmneg  11744  isprm6  11814  cncongrprm  11824  phimullem  11890  tgcl  12222  tgclb  12223  tgss2  12237  ntrss3  12281  ntridm  12284  opnssneib  12314  ssnei2  12315  innei  12321  resttopon  12329  cnpnei  12377  cnntri  12382  lmss  12404  txcnp  12429  blpnfctr  12597  mopni2  12641  bdmopn  12662  climcncf  12729  ivthdec  12780  cnplimcim  12794  dvconst  12819  dvef  12845  cvgcmp2nlemabs  13216  trilpolemisumle  13220  trilpolemeq1  13222  trilpolemlt1  13223