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

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

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 1011

This theorem is referenced by:  fvun1  5766  caseinl  7425  caseinr  7426  reapmul1  8917  recrecap  9033  rec11rap  9035  divdivdivap  9037  dmdcanap  9046  ddcanap  9050  rerecclap  9054  div2negap  9059  divap1d  9125  divmulapd  9136  apdivmuld  9137  divmulap2d  9148  divmulap3d  9149  divassapd  9150  div12apd  9151  div23apd  9152  divdirapd  9153  divsubdirapd  9154  div11apd  9155  ltmul12a  9184  ltdiv1  9192  ltrec  9207  lt2msq1  9209  lediv2  9215  lediv23  9217  recp1lt1  9223  qapne  10022  xadd4d  10270  xleaddadd  10272  modqge0  10752  modqlt  10753  modqid  10769  expgt1  10997  nnlesq  11063  expnbnd  11084  facubnd  11166  pfxsuffeqwrdeq  11453  resqrexlemover  11759  mulcn2  12061  cvgratnnlemnexp  12274  cvgratnnlemmn  12275  eftlub  12440  eflegeo  12451  sin01bnd  12507  cos01bnd  12508  eirraplem  12527  bitsmod  12706  bezoutlemnewy  12756  bezoutlemstep  12757  mulgcd  12776  mulgcddvds  12855  prmind2  12881  oddpwdclemxy  12930  oddpwdclemodd  12933  qnumgt0  12959  pcpremul  13055  fldivp1  13110  pcfaclem  13111  qexpz  13114  prmpwdvds  13117  pockthg  13119  4sqlem10  13149  4sqlem12  13164  4sqlem16  13168  4sqlem17  13169  ablsub4  14100  znrrg  14978  txdis  15361  txdis1cn  15362  xblm  15501  reeff1oleme  15856  tangtx  15922  cosordlem  15933  logdivlti  15965  apcxp2  16024  log2tlbndlog2  16065  birthdaylem3  16072  pellexlem2  16075  mersenne  16094  lgsdilem  16129  lgseisenlem1  16172  lgseisenlem2  16173  lgseisenlem3  16174  lgsquadlem1  16179  lgsquadlem2  16180  2sqlem3  16219  2sqlem8  16225  0uhgrsubgr  16489  eupth2lem3lem3fi  16694  apdifflemr  17070