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  5715  caseinl  7295  caseinr  7296  reapmul1  8780  recrecap  8894  rec11rap  8896  divdivdivap  8898  dmdcanap  8907  ddcanap  8911  rerecclap  8915  div2negap  8920  divap1d  8986  divmulapd  8997  apdivmuld  8998  divmulap2d  9009  divmulap3d  9010  divassapd  9011  div12apd  9012  div23apd  9013  divdirapd  9014  divsubdirapd  9015  div11apd  9016  ltmul12a  9045  ltdiv1  9053  ltrec  9068  lt2msq1  9070  lediv2  9076  lediv23  9078  recp1lt1  9084  qapne  9878  xadd4d  10125  xleaddadd  10127  modqge0  10600  modqlt  10601  modqid  10617  expgt1  10845  nnlesq  10911  expnbnd  10931  facubnd  11013  pfxsuffeqwrdeq  11288  resqrexlemover  11593  mulcn2  11895  cvgratnnlemnexp  12108  cvgratnnlemmn  12109  eftlub  12274  eflegeo  12285  sin01bnd  12341  cos01bnd  12342  eirraplem  12361  bitsmod  12540  bezoutlemnewy  12590  bezoutlemstep  12591  mulgcd  12610  mulgcddvds  12689  prmind2  12715  oddpwdclemxy  12764  oddpwdclemodd  12767  qnumgt0  12793  pcpremul  12889  fldivp1  12944  pcfaclem  12945  qexpz  12948  prmpwdvds  12951  pockthg  12953  4sqlem10  12983  4sqlem12  12998  4sqlem16  13002  4sqlem17  13003  ablsub4  13923  znrrg  14698  txdis  15030  txdis1cn  15031  xblm  15170  reeff1oleme  15525  tangtx  15591  cosordlem  15602  logdivlti  15634  apcxp2  15692  mersenne  15750  lgsdilem  15785  lgseisenlem1  15828  lgseisenlem2  15829  lgseisenlem3  15830  lgsquadlem1  15835  lgsquadlem2  15836  2sqlem3  15875  2sqlem8  15881  0uhgrsubgr  16145  eupth2lem3lem3fi  16350  apdifflemr  16718