Theorem syl112anc 1173

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
sylXanc.1	⊢ (𝜑 → 𝜓)
sylXanc.2	⊢ (𝜑 → 𝜒)
sylXanc.3	⊢ (𝜑 → 𝜃)
sylXanc.4	⊢ (𝜑 → 𝜏)
syl112anc.5	⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂)

Assertion

Ref	Expression
syl112anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl112anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. 2 ⊢ (𝜑 → 𝜓)
2		sylXanc.2	. 2 ⊢ (𝜑 → 𝜒)
3		sylXanc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		sylXanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5	3, 4	jca 300	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏))
6		syl112anc.5	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	1, 2, 5, 6	syl3anc 1169	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  fvun1  5260  reapmul1  7695  recrecap  7797  rec11rap  7799  divdivdivap  7801  dmdcanap  7810  ddcanap  7814  rerecclap  7818  div2negap  7823  divap1d  7888  divmulapd  7899  divmulap2d  7910  divmulap3d  7911  divassapd  7912  div12apd  7913  div23apd  7914  divdirapd  7915  divsubdirapd  7916  div11apd  7917  ltmul12a  7938  ltdiv1  7946  ltrec  7961  lt2msq1  7963  lediv2  7969  lediv23  7971  recp1lt1  7977  qapne  8724  modqge0  9334  modqlt  9335  modqid  9351  expgt1  9514  nnlesq  9578  expnbnd  9596  facubnd  9672  resqrexlemover  9896  mulcn2  10151  bezoutlemnewy  10385  bezoutlemstep  10386  mulgcd  10405  mulgcddvds  10476  prmind2  10502  oddpwdclemxy  10547  oddpwdclemodd  10550