Theorem syl112anc 1256

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

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

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 985

This theorem is referenced by:  fvun1  5673  caseinl  7226  caseinr  7227  reapmul1  8710  recrecap  8824  rec11rap  8826  divdivdivap  8828  dmdcanap  8837  ddcanap  8841  rerecclap  8845  div2negap  8850  divap1d  8916  divmulapd  8927  apdivmuld  8928  divmulap2d  8939  divmulap3d  8940  divassapd  8941  div12apd  8942  div23apd  8943  divdirapd  8944  divsubdirapd  8945  div11apd  8946  ltmul12a  8975  ltdiv1  8983  ltrec  8998  lt2msq1  9000  lediv2  9006  lediv23  9008  recp1lt1  9014  qapne  9802  xadd4d  10049  xleaddadd  10051  modqge0  10521  modqlt  10522  modqid  10538  expgt1  10766  nnlesq  10832  expnbnd  10852  facubnd  10934  pfxsuffeqwrdeq  11196  resqrexlemover  11487  mulcn2  11789  cvgratnnlemnexp  12001  cvgratnnlemmn  12002  eftlub  12167  eflegeo  12178  sin01bnd  12234  cos01bnd  12235  eirraplem  12254  bitsmod  12433  bezoutlemnewy  12483  bezoutlemstep  12484  mulgcd  12503  mulgcddvds  12582  prmind2  12608  oddpwdclemxy  12657  oddpwdclemodd  12660  qnumgt0  12686  pcpremul  12782  fldivp1  12837  pcfaclem  12838  qexpz  12841  prmpwdvds  12844  pockthg  12846  4sqlem10  12876  4sqlem12  12891  4sqlem16  12895  4sqlem17  12896  ablsub4  13816  znrrg  14589  txdis  14916  txdis1cn  14917  xblm  15056  reeff1oleme  15411  tangtx  15477  cosordlem  15488  logdivlti  15520  apcxp2  15578  mersenne  15636  lgsdilem  15671  lgseisenlem1  15714  lgseisenlem2  15715  lgseisenlem3  15716  lgsquadlem1  15721  lgsquadlem2  15722  2sqlem3  15761  2sqlem8  15767  apdifflemr  16326