Theorem syl112anc 1253

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

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

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 982

This theorem is referenced by:  fvun1  5624  caseinl  7152  caseinr  7153  reapmul1  8616  recrecap  8730  rec11rap  8732  divdivdivap  8734  dmdcanap  8743  ddcanap  8747  rerecclap  8751  div2negap  8756  divap1d  8822  divmulapd  8833  apdivmuld  8834  divmulap2d  8845  divmulap3d  8846  divassapd  8847  div12apd  8848  div23apd  8849  divdirapd  8850  divsubdirapd  8851  div11apd  8852  ltmul12a  8881  ltdiv1  8889  ltrec  8904  lt2msq1  8906  lediv2  8912  lediv23  8914  recp1lt1  8920  qapne  9707  xadd4d  9954  xleaddadd  9956  modqge0  10406  modqlt  10407  modqid  10423  expgt1  10651  nnlesq  10717  expnbnd  10737  facubnd  10819  resqrexlemover  11157  mulcn2  11458  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  eftlub  11836  eflegeo  11847  sin01bnd  11903  cos01bnd  11904  eirraplem  11923  bezoutlemnewy  12136  bezoutlemstep  12137  mulgcd  12156  mulgcddvds  12235  prmind2  12261  oddpwdclemxy  12310  oddpwdclemodd  12313  qnumgt0  12339  pcpremul  12434  fldivp1  12489  pcfaclem  12490  qexpz  12493  prmpwdvds  12496  pockthg  12498  4sqlem10  12528  4sqlem12  12543  4sqlem16  12547  4sqlem17  12548  ablsub4  13386  znrrg  14159  txdis  14456  txdis1cn  14457  xblm  14596  reeff1oleme  14948  tangtx  15014  cosordlem  15025  logdivlti  15057  apcxp2  15113  lgsdilem  15184  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgsquadlem1  15234  lgsquadlem2  15235  2sqlem3  15274  2sqlem8  15280  apdifflemr  15607