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  5702  caseinl  7266  caseinr  7267  reapmul1  8750  recrecap  8864  rec11rap  8866  divdivdivap  8868  dmdcanap  8877  ddcanap  8881  rerecclap  8885  div2negap  8890  divap1d  8956  divmulapd  8967  apdivmuld  8968  divmulap2d  8979  divmulap3d  8980  divassapd  8981  div12apd  8982  div23apd  8983  divdirapd  8984  divsubdirapd  8985  div11apd  8986  ltmul12a  9015  ltdiv1  9023  ltrec  9038  lt2msq1  9040  lediv2  9046  lediv23  9048  recp1lt1  9054  qapne  9842  xadd4d  10089  xleaddadd  10091  modqge0  10562  modqlt  10563  modqid  10579  expgt1  10807  nnlesq  10873  expnbnd  10893  facubnd  10975  pfxsuffeqwrdeq  11238  resqrexlemover  11529  mulcn2  11831  cvgratnnlemnexp  12043  cvgratnnlemmn  12044  eftlub  12209  eflegeo  12220  sin01bnd  12276  cos01bnd  12277  eirraplem  12296  bitsmod  12475  bezoutlemnewy  12525  bezoutlemstep  12526  mulgcd  12545  mulgcddvds  12624  prmind2  12650  oddpwdclemxy  12699  oddpwdclemodd  12702  qnumgt0  12728  pcpremul  12824  fldivp1  12879  pcfaclem  12880  qexpz  12883  prmpwdvds  12886  pockthg  12888  4sqlem10  12918  4sqlem12  12933  4sqlem16  12937  4sqlem17  12938  ablsub4  13858  znrrg  14632  txdis  14959  txdis1cn  14960  xblm  15099  reeff1oleme  15454  tangtx  15520  cosordlem  15531  logdivlti  15563  apcxp2  15621  mersenne  15679  lgsdilem  15714  lgseisenlem1  15757  lgseisenlem2  15758  lgseisenlem3  15759  lgsquadlem1  15764  lgsquadlem2  15765  2sqlem3  15804  2sqlem8  15810  apdifflemr  16445