Theorem syl112anc 1220

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 304	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏))
6		syl112anc.5	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	1, 2, 5, 6	syl3anc 1216	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 962

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  fvun1  5480  caseinl  6969  caseinr  6970  reapmul1  8350  recrecap  8462  rec11rap  8464  divdivdivap  8466  dmdcanap  8475  ddcanap  8479  rerecclap  8483  div2negap  8488  divap1d  8554  divmulapd  8565  apdivmuld  8566  divmulap2d  8577  divmulap3d  8578  divassapd  8579  div12apd  8580  div23apd  8581  divdirapd  8582  divsubdirapd  8583  div11apd  8584  ltmul12a  8611  ltdiv1  8619  ltrec  8634  lt2msq1  8636  lediv2  8642  lediv23  8644  recp1lt1  8650  qapne  9424  xadd4d  9661  xleaddadd  9663  modqge0  10098  modqlt  10099  modqid  10115  expgt1  10324  nnlesq  10389  expnbnd  10408  facubnd  10484  resqrexlemover  10775  mulcn2  11074  cvgratnnlemnexp  11286  cvgratnnlemmn  11287  eftlub  11385  eflegeo  11397  sin01bnd  11453  cos01bnd  11454  eirraplem  11472  bezoutlemnewy  11673  bezoutlemstep  11674  mulgcd  11693  mulgcddvds  11764  prmind2  11790  oddpwdclemxy  11836  oddpwdclemodd  11839  qnumgt0  11865  txdis  12435  txdis1cn  12436  xblm  12575  tangtx  12908  cosordlem  12919