Theorem syl112anc 1275

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

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

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 1004

This theorem is referenced by:  fvun1  5700  caseinl  7258  caseinr  7259  reapmul1  8742  recrecap  8856  rec11rap  8858  divdivdivap  8860  dmdcanap  8869  ddcanap  8873  rerecclap  8877  div2negap  8882  divap1d  8948  divmulapd  8959  apdivmuld  8960  divmulap2d  8971  divmulap3d  8972  divassapd  8973  div12apd  8974  div23apd  8975  divdirapd  8976  divsubdirapd  8977  div11apd  8978  ltmul12a  9007  ltdiv1  9015  ltrec  9030  lt2msq1  9032  lediv2  9038  lediv23  9040  recp1lt1  9046  qapne  9834  xadd4d  10081  xleaddadd  10083  modqge0  10554  modqlt  10555  modqid  10571  expgt1  10799  nnlesq  10865  expnbnd  10885  facubnd  10967  pfxsuffeqwrdeq  11230  resqrexlemover  11521  mulcn2  11823  cvgratnnlemnexp  12035  cvgratnnlemmn  12036  eftlub  12201  eflegeo  12212  sin01bnd  12268  cos01bnd  12269  eirraplem  12288  bitsmod  12467  bezoutlemnewy  12517  bezoutlemstep  12518  mulgcd  12537  mulgcddvds  12616  prmind2  12642  oddpwdclemxy  12691  oddpwdclemodd  12694  qnumgt0  12720  pcpremul  12816  fldivp1  12871  pcfaclem  12872  qexpz  12875  prmpwdvds  12878  pockthg  12880  4sqlem10  12910  4sqlem12  12925  4sqlem16  12929  4sqlem17  12930  ablsub4  13850  znrrg  14624  txdis  14951  txdis1cn  14952  xblm  15091  reeff1oleme  15446  tangtx  15512  cosordlem  15523  logdivlti  15555  apcxp2  15613  mersenne  15671  lgsdilem  15706  lgseisenlem1  15749  lgseisenlem2  15750  lgseisenlem3  15751  lgsquadlem1  15756  lgsquadlem2  15757  2sqlem3  15796  2sqlem8  15802  apdifflemr  16415