Theorem syl112anc 1275

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

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

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 1004

This theorem is referenced by:  fvun1  5708  caseinl  7284  caseinr  7285  reapmul1  8768  recrecap  8882  rec11rap  8884  divdivdivap  8886  dmdcanap  8895  ddcanap  8899  rerecclap  8903  div2negap  8908  divap1d  8974  divmulapd  8985  apdivmuld  8986  divmulap2d  8997  divmulap3d  8998  divassapd  8999  div12apd  9000  div23apd  9001  divdirapd  9002  divsubdirapd  9003  div11apd  9004  ltmul12a  9033  ltdiv1  9041  ltrec  9056  lt2msq1  9058  lediv2  9064  lediv23  9066  recp1lt1  9072  qapne  9866  xadd4d  10113  xleaddadd  10115  modqge0  10587  modqlt  10588  modqid  10604  expgt1  10832  nnlesq  10898  expnbnd  10918  facubnd  11000  pfxsuffeqwrdeq  11272  resqrexlemover  11564  mulcn2  11866  cvgratnnlemnexp  12078  cvgratnnlemmn  12079  eftlub  12244  eflegeo  12255  sin01bnd  12311  cos01bnd  12312  eirraplem  12331  bitsmod  12510  bezoutlemnewy  12560  bezoutlemstep  12561  mulgcd  12580  mulgcddvds  12659  prmind2  12685  oddpwdclemxy  12734  oddpwdclemodd  12737  qnumgt0  12763  pcpremul  12859  fldivp1  12914  pcfaclem  12915  qexpz  12918  prmpwdvds  12921  pockthg  12923  4sqlem10  12953  4sqlem12  12968  4sqlem16  12972  4sqlem17  12973  ablsub4  13893  znrrg  14667  txdis  14994  txdis1cn  14995  xblm  15134  reeff1oleme  15489  tangtx  15555  cosordlem  15566  logdivlti  15598  apcxp2  15656  mersenne  15714  lgsdilem  15749  lgseisenlem1  15792  lgseisenlem2  15793  lgseisenlem3  15794  lgsquadlem1  15799  lgsquadlem2  15800  2sqlem3  15839  2sqlem8  15845  apdifflemr  16601