Theorem sylanbrc 645

Description: Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
sylanbrc.1	⊢ (φ → ψ)
sylanbrc.2	⊢ (φ → χ)
sylanbrc.3	⊢ (θ ↔ (ψ ∧ χ))

Assertion

Ref	Expression
sylanbrc	⊢ (φ → θ)

Proof of Theorem sylanbrc

Step	Hyp	Ref	Expression
1		sylanbrc.1	. . 3 ⊢ (φ → ψ)
2		sylanbrc.2	. . 3 ⊢ (φ → χ)
3	1, 2	jca 518	. 2 ⊢ (φ → (ψ ∧ χ))
4		sylanbrc.3	. 2 ⊢ (θ ↔ (ψ ∧ χ))
5	3, 4	sylibr 203	1 ⊢ (φ → θ)

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  ecase23d  1285  sbequ1  1918  sb2  2023  sbn  2062  eqeu  3007  euind  3023  reuind  3039  eqssd  3289  ssrabdv  3345  psstr  3373  vfinnc  4471  nnpw1ex  4484  evenoddnnnul  4514  sfinltfin  4535  sfin111  4536  imainss  5042  ssdmrn  5099  fnprg  5153  fnco  5191  f00  5249  f1ss  5262  f1f1orn  5297  foimacnv  5303  fun11iun  5305  dff3  5420  foco2  5426  ffnfv  5427  ffvresb  5431  isoini2  5498  f1oiso  5499  fnoprabg  5585  fmpt  5692  fmpt2d  5695  f1od  5726  sod  5937  so0  5941  iserd  5942  enpw1  6062  ncspw1eu  6159  ltcpw1pwg  6202  nchoicelem17  6305  nchoice  6308  fnfrec  6320