Theorem syl112anc 1278

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

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

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 1007

This theorem is referenced by:  fvun1  5742  caseinl  7381  caseinr  7382  reapmul1  8865  recrecap  8979  rec11rap  8981  divdivdivap  8983  dmdcanap  8992  ddcanap  8996  rerecclap  9000  div2negap  9005  divap1d  9071  divmulapd  9082  apdivmuld  9083  divmulap2d  9094  divmulap3d  9095  divassapd  9096  div12apd  9097  div23apd  9098  divdirapd  9099  divsubdirapd  9100  div11apd  9101  ltmul12a  9130  ltdiv1  9138  ltrec  9153  lt2msq1  9155  lediv2  9161  lediv23  9163  recp1lt1  9169  qapne  9967  xadd4d  10214  xleaddadd  10216  modqge0  10690  modqlt  10691  modqid  10707  expgt1  10935  nnlesq  11001  expnbnd  11021  facubnd  11103  pfxsuffeqwrdeq  11383  resqrexlemover  11688  mulcn2  11990  cvgratnnlemnexp  12203  cvgratnnlemmn  12204  eftlub  12369  eflegeo  12380  sin01bnd  12436  cos01bnd  12437  eirraplem  12456  bitsmod  12635  bezoutlemnewy  12685  bezoutlemstep  12686  mulgcd  12705  mulgcddvds  12784  prmind2  12810  oddpwdclemxy  12859  oddpwdclemodd  12862  qnumgt0  12888  pcpremul  12984  fldivp1  13039  pcfaclem  13040  qexpz  13043  prmpwdvds  13046  pockthg  13048  4sqlem10  13078  4sqlem12  13093  4sqlem16  13097  4sqlem17  13098  ablsub4  14019  znrrg  14795  txdis  15129  txdis1cn  15130  xblm  15269  reeff1oleme  15624  tangtx  15690  cosordlem  15701  logdivlti  15733  apcxp2  15791  pellexlem2  15833  mersenne  15852  lgsdilem  15887  lgseisenlem1  15930  lgseisenlem2  15931  lgseisenlem3  15932  lgsquadlem1  15937  lgsquadlem2  15938  2sqlem3  15977  2sqlem8  15983  0uhgrsubgr  16247  eupth2lem3lem3fi  16452  apdifflemr  16818