Theorem syl112anc 1282

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  fvun1  5769  caseinl  7431  caseinr  7432  reapmul1  8924  recrecap  9040  rec11rap  9042  divdivdivap  9044  dmdcanap  9053  ddcanap  9057  rerecclap  9061  div2negap  9066  divap1d  9132  divmulapd  9143  apdivmuld  9144  divmulap2d  9155  divmulap3d  9156  divassapd  9157  div12apd  9158  div23apd  9159  divdirapd  9160  divsubdirapd  9161  div11apd  9162  ltmul12a  9191  ltdiv1  9199  ltrec  9214  lt2msq1  9216  lediv2  9222  lediv23  9224  recp1lt1  9230  qapne  10041  xadd4d  10289  xleaddadd  10291  modqge0  10771  modqlt  10772  modqid  10788  expgt1  11016  nnlesq  11082  expnbnd  11103  facubnd  11185  pfxsuffeqwrdeq  11472  resqrexlemover  11778  mulcn2  12080  cvgratnnlemnexp  12293  cvgratnnlemmn  12294  eftlub  12459  eflegeo  12470  sin01bnd  12526  cos01bnd  12527  eirraplem  12546  bitsmod  12725  bezoutlemnewy  12775  bezoutlemstep  12776  mulgcd  12795  mulgcddvds  12874  prmind2  12900  oddpwdclemxy  12949  oddpwdclemodd  12952  qnumgt0  12978  pcpremul  13074  fldivp1  13129  pcfaclem  13130  qexpz  13133  prmpwdvds  13136  pockthg  13138  4sqlem10  13168  4sqlem12  13183  4sqlem16  13187  4sqlem17  13188  ablsub4  14119  znrrg  14997  txdis  15380  txdis1cn  15381  xblm  15520  reeff1oleme  15875  tangtx  15942  cosordlem  15953  logdivlti  15986  apcxp2  16047  log2tlbndlog2  16088  birthdaylem3  16095  pellexlem2  16098  mersenne  16117  lgsdilem  16158  lgseisenlem1  16201  lgseisenlem2  16202  lgseisenlem3  16203  lgsquadlem1  16208  lgsquadlem2  16209  2sqlem3  16248  2sqlem8  16254  0uhgrsubgr  16518  eupth2lem3lem3fi  16723  apdifflemr  17108