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  5705  caseinl  7274  caseinr  7275  reapmul1  8758  recrecap  8872  rec11rap  8874  divdivdivap  8876  dmdcanap  8885  ddcanap  8889  rerecclap  8893  div2negap  8898  divap1d  8964  divmulapd  8975  apdivmuld  8976  divmulap2d  8987  divmulap3d  8988  divassapd  8989  div12apd  8990  div23apd  8991  divdirapd  8992  divsubdirapd  8993  div11apd  8994  ltmul12a  9023  ltdiv1  9031  ltrec  9046  lt2msq1  9048  lediv2  9054  lediv23  9056  recp1lt1  9062  qapne  9851  xadd4d  10098  xleaddadd  10100  modqge0  10571  modqlt  10572  modqid  10588  expgt1  10816  nnlesq  10882  expnbnd  10902  facubnd  10984  pfxsuffeqwrdeq  11251  resqrexlemover  11542  mulcn2  11844  cvgratnnlemnexp  12056  cvgratnnlemmn  12057  eftlub  12222  eflegeo  12233  sin01bnd  12289  cos01bnd  12290  eirraplem  12309  bitsmod  12488  bezoutlemnewy  12538  bezoutlemstep  12539  mulgcd  12558  mulgcddvds  12637  prmind2  12663  oddpwdclemxy  12712  oddpwdclemodd  12715  qnumgt0  12741  pcpremul  12837  fldivp1  12892  pcfaclem  12893  qexpz  12896  prmpwdvds  12899  pockthg  12901  4sqlem10  12931  4sqlem12  12946  4sqlem16  12950  4sqlem17  12951  ablsub4  13871  znrrg  14645  txdis  14972  txdis1cn  14973  xblm  15112  reeff1oleme  15467  tangtx  15533  cosordlem  15544  logdivlti  15576  apcxp2  15634  mersenne  15692  lgsdilem  15727  lgseisenlem1  15770  lgseisenlem2  15771  lgseisenlem3  15772  lgsquadlem1  15777  lgsquadlem2  15778  2sqlem3  15817  2sqlem8  15823  apdifflemr  16529