Theorem syl112anc 1254

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

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

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 983

This theorem is referenced by:  fvun1  5652  caseinl  7200  caseinr  7201  reapmul1  8675  recrecap  8789  rec11rap  8791  divdivdivap  8793  dmdcanap  8802  ddcanap  8806  rerecclap  8810  div2negap  8815  divap1d  8881  divmulapd  8892  apdivmuld  8893  divmulap2d  8904  divmulap3d  8905  divassapd  8906  div12apd  8907  div23apd  8908  divdirapd  8909  divsubdirapd  8910  div11apd  8911  ltmul12a  8940  ltdiv1  8948  ltrec  8963  lt2msq1  8965  lediv2  8971  lediv23  8973  recp1lt1  8979  qapne  9767  xadd4d  10014  xleaddadd  10016  modqge0  10484  modqlt  10485  modqid  10501  expgt1  10729  nnlesq  10795  expnbnd  10815  facubnd  10897  pfxsuffeqwrdeq  11157  resqrexlemover  11365  mulcn2  11667  cvgratnnlemnexp  11879  cvgratnnlemmn  11880  eftlub  12045  eflegeo  12056  sin01bnd  12112  cos01bnd  12113  eirraplem  12132  bitsmod  12311  bezoutlemnewy  12361  bezoutlemstep  12362  mulgcd  12381  mulgcddvds  12460  prmind2  12486  oddpwdclemxy  12535  oddpwdclemodd  12538  qnumgt0  12564  pcpremul  12660  fldivp1  12715  pcfaclem  12716  qexpz  12719  prmpwdvds  12722  pockthg  12724  4sqlem10  12754  4sqlem12  12769  4sqlem16  12773  4sqlem17  12774  ablsub4  13693  znrrg  14466  txdis  14793  txdis1cn  14794  xblm  14933  reeff1oleme  15288  tangtx  15354  cosordlem  15365  logdivlti  15397  apcxp2  15455  mersenne  15513  lgsdilem  15548  lgseisenlem1  15591  lgseisenlem2  15592  lgseisenlem3  15593  lgsquadlem1  15598  lgsquadlem2  15599  2sqlem3  15638  2sqlem8  15644  apdifflemr  16060