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  5630  caseinl  7166  caseinr  7167  reapmul1  8641  recrecap  8755  rec11rap  8757  divdivdivap  8759  dmdcanap  8768  ddcanap  8772  rerecclap  8776  div2negap  8781  divap1d  8847  divmulapd  8858  apdivmuld  8859  divmulap2d  8870  divmulap3d  8871  divassapd  8872  div12apd  8873  div23apd  8874  divdirapd  8875  divsubdirapd  8876  div11apd  8877  ltmul12a  8906  ltdiv1  8914  ltrec  8929  lt2msq1  8931  lediv2  8937  lediv23  8939  recp1lt1  8945  qapne  9732  xadd4d  9979  xleaddadd  9981  modqge0  10443  modqlt  10444  modqid  10460  expgt1  10688  nnlesq  10754  expnbnd  10774  facubnd  10856  resqrexlemover  11194  mulcn2  11496  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  eftlub  11874  eflegeo  11885  sin01bnd  11941  cos01bnd  11942  eirraplem  11961  bitsmod  12140  bezoutlemnewy  12190  bezoutlemstep  12191  mulgcd  12210  mulgcddvds  12289  prmind2  12315  oddpwdclemxy  12364  oddpwdclemodd  12367  qnumgt0  12393  pcpremul  12489  fldivp1  12544  pcfaclem  12545  qexpz  12548  prmpwdvds  12551  pockthg  12553  4sqlem10  12583  4sqlem12  12598  4sqlem16  12602  4sqlem17  12603  ablsub4  13521  znrrg  14294  txdis  14621  txdis1cn  14622  xblm  14761  reeff1oleme  15116  tangtx  15182  cosordlem  15193  logdivlti  15225  apcxp2  15283  mersenne  15341  lgsdilem  15376  lgseisenlem1  15419  lgseisenlem2  15420  lgseisenlem3  15421  lgsquadlem1  15426  lgsquadlem2  15427  2sqlem3  15466  2sqlem8  15472  apdifflemr  15804