Theorem syl112anc 1174

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 1170	1 ⊢ (𝜑 → 𝜂)

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

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 922

This theorem is referenced by:  fvun1  5265  reapmul1  7751  recrecap  7853  rec11rap  7855  divdivdivap  7857  dmdcanap  7866  ddcanap  7870  rerecclap  7874  div2negap  7879  divap1d  7944  divmulapd  7955  divmulap2d  7966  divmulap3d  7967  divassapd  7968  div12apd  7969  div23apd  7970  divdirapd  7971  divsubdirapd  7972  div11apd  7973  ltmul12a  7994  ltdiv1  8002  ltrec  8017  lt2msq1  8019  lediv2  8025  lediv23  8027  recp1lt1  8033  qapne  8794  modqge0  9403  modqlt  9404  modqid  9420  expgt1  9600  nnlesq  9664  expnbnd  9682  facubnd  9758  resqrexlemover  10023  mulcn2  10278  bezoutlemnewy  10518  bezoutlemstep  10519  mulgcd  10538  mulgcddvds  10609  prmind2  10635  oddpwdclemxy  10680  oddpwdclemodd  10683