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  5603  caseinl  7120  caseinr  7121  reapmul1  8582  recrecap  8696  rec11rap  8698  divdivdivap  8700  dmdcanap  8709  ddcanap  8713  rerecclap  8717  div2negap  8722  divap1d  8788  divmulapd  8799  apdivmuld  8800  divmulap2d  8811  divmulap3d  8812  divassapd  8813  div12apd  8814  div23apd  8815  divdirapd  8816  divsubdirapd  8817  div11apd  8818  ltmul12a  8847  ltdiv1  8855  ltrec  8870  lt2msq1  8872  lediv2  8878  lediv23  8880  recp1lt1  8886  qapne  9669  xadd4d  9915  xleaddadd  9917  modqge0  10363  modqlt  10364  modqid  10380  expgt1  10589  nnlesq  10655  expnbnd  10675  facubnd  10757  resqrexlemover  11051  mulcn2  11352  cvgratnnlemnexp  11564  cvgratnnlemmn  11565  eftlub  11730  eflegeo  11741  sin01bnd  11797  cos01bnd  11798  eirraplem  11816  bezoutlemnewy  12029  bezoutlemstep  12030  mulgcd  12049  mulgcddvds  12126  prmind2  12152  oddpwdclemxy  12201  oddpwdclemodd  12204  qnumgt0  12230  pcpremul  12325  fldivp1  12380  pcfaclem  12381  qexpz  12384  prmpwdvds  12387  pockthg  12389  4sqlem10  12419  4sqlem12  12434  4sqlem16  12438  4sqlem17  12439  ablsub4  13252  txdis  14234  txdis1cn  14235  xblm  14374  reeff1oleme  14650  tangtx  14716  cosordlem  14727  logdivlti  14759  apcxp2  14815  lgsdilem  14886  lgseisenlem1  14908  lgseisenlem2  14909  2sqlem3  14922  2sqlem8  14928  apdifflemr  15254