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  5487  caseinl  6976  caseinr  6977  reapmul1  8357  recrecap  8469  rec11rap  8471  divdivdivap  8473  dmdcanap  8482  ddcanap  8486  rerecclap  8490  div2negap  8495  divap1d  8561  divmulapd  8572  apdivmuld  8573  divmulap2d  8584  divmulap3d  8585  divassapd  8586  div12apd  8587  div23apd  8588  divdirapd  8589  divsubdirapd  8590  div11apd  8591  ltmul12a  8618  ltdiv1  8626  ltrec  8641  lt2msq1  8643  lediv2  8649  lediv23  8651  recp1lt1  8657  qapne  9431  xadd4d  9668  xleaddadd  9670  modqge0  10105  modqlt  10106  modqid  10122  expgt1  10331  nnlesq  10396  expnbnd  10415  facubnd  10491  resqrexlemover  10782  mulcn2  11081  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  eftlub  11396  eflegeo  11408  sin01bnd  11464  cos01bnd  11465  eirraplem  11483  bezoutlemnewy  11684  bezoutlemstep  11685  mulgcd  11704  mulgcddvds  11775  prmind2  11801  oddpwdclemxy  11847  oddpwdclemodd  11850  qnumgt0  11876  txdis  12446  txdis1cn  12447  xblm  12586  tangtx  12919  cosordlem  12930