Theorem syl112anc 1277

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1004

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

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  fvun1  5712  caseinl  7290  caseinr  7291  reapmul1  8775  recrecap  8889  rec11rap  8891  divdivdivap  8893  dmdcanap  8902  ddcanap  8906  rerecclap  8910  div2negap  8915  divap1d  8981  divmulapd  8992  apdivmuld  8993  divmulap2d  9004  divmulap3d  9005  divassapd  9006  div12apd  9007  div23apd  9008  divdirapd  9009  divsubdirapd  9010  div11apd  9011  ltmul12a  9040  ltdiv1  9048  ltrec  9063  lt2msq1  9065  lediv2  9071  lediv23  9073  recp1lt1  9079  qapne  9873  xadd4d  10120  xleaddadd  10122  modqge0  10595  modqlt  10596  modqid  10612  expgt1  10840  nnlesq  10906  expnbnd  10926  facubnd  11008  pfxsuffeqwrdeq  11280  resqrexlemover  11572  mulcn2  11874  cvgratnnlemnexp  12087  cvgratnnlemmn  12088  eftlub  12253  eflegeo  12264  sin01bnd  12320  cos01bnd  12321  eirraplem  12340  bitsmod  12519  bezoutlemnewy  12569  bezoutlemstep  12570  mulgcd  12589  mulgcddvds  12668  prmind2  12694  oddpwdclemxy  12743  oddpwdclemodd  12746  qnumgt0  12772  pcpremul  12868  fldivp1  12923  pcfaclem  12924  qexpz  12927  prmpwdvds  12930  pockthg  12932  4sqlem10  12962  4sqlem12  12977  4sqlem16  12981  4sqlem17  12982  ablsub4  13902  znrrg  14677  txdis  15004  txdis1cn  15005  xblm  15144  reeff1oleme  15499  tangtx  15565  cosordlem  15576  logdivlti  15608  apcxp2  15666  mersenne  15724  lgsdilem  15759  lgseisenlem1  15802  lgseisenlem2  15803  lgseisenlem3  15804  lgsquadlem1  15809  lgsquadlem2  15810  2sqlem3  15849  2sqlem8  15855  0uhgrsubgr  16119  eupth2lem3lem3fi  16324  apdifflemr  16672