Theorem syl112anc 1282

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  fvun1  5772  caseinl  7438  caseinr  7439  reapmul1  8932  recrecap  9048  rec11rap  9050  divdivdivap  9052  dmdcanap  9061  ddcanap  9065  rerecclap  9069  div2negap  9074  divap1d  9140  divmulapd  9151  apdivmuld  9152  divmulap2d  9163  divmulap3d  9164  divassapd  9165  div12apd  9166  div23apd  9167  divdirapd  9168  divsubdirapd  9169  div11apd  9170  ltmul12a  9199  ltdiv1  9207  ltrec  9222  lt2msq1  9224  lediv2  9230  lediv23  9232  recp1lt1  9238  qapne  10056  xadd4d  10305  xleaddadd  10307  modqge0  10791  modqlt  10792  modqid  10808  expgt1  11036  nnlesq  11102  expnbnd  11123  facubnd  11206  pfxsuffeqwrdeq  11493  resqrexlemover  11799  mulcn2  12104  cvgratnnlemnexp  12317  cvgratnnlemmn  12318  eftlub  12483  eflegeo  12494  sin01bnd  12550  cos01bnd  12551  eirraplem  12570  bitsmod  12749  bezoutlemnewy  12799  bezoutlemstep  12800  mulgcd  12819  mulgcddvds  12898  prmind2  12924  nnmaxpwlemxy  12974  nnmaxpwlemnfac  12977  qnumgt0  13004  pcpremul  13102  fldivp1  13157  pcfaclem  13158  qexpz  13161  prmpwdvds  13164  pockthg  13166  4sqlem10  13196  4sqlem12  13211  4sqlem16  13215  4sqlem17  13216  ablsub4  14208  znrrg  15105  txdis  15515  txdis1cn  15516  xblm  15655  reeff1oleme  16010  tangtx  16077  cosordlem  16089  logdivlti  16123  apcxp2  16186  zprmlogbaplem3  16229  log2tlbndlog2  16232  birthdaylem3  16239  pellexlem2  16242  ppiqub  16305  mersenne  16309  bposlem1  16323  bposlem2  16324  bposlem4  16326  lgsdilem  16363  lgseisenlem1  16406  lgseisenlem2  16407  lgseisenlem3  16408  lgsquadlem1  16413  lgsquadlem2  16414  2sqlem3  16453  2sqlem8  16459  0uhgrsubgr  16723  eupth2lem3lem3fi  16928  apdifflemr  17315