Theorem syl112anc 1278

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

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

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 1007

This theorem is referenced by:  fvun1  5748  caseinl  7395  caseinr  7396  reapmul1  8887  recrecap  9003  rec11rap  9005  divdivdivap  9007  dmdcanap  9016  ddcanap  9020  rerecclap  9024  div2negap  9029  divap1d  9095  divmulapd  9106  apdivmuld  9107  divmulap2d  9118  divmulap3d  9119  divassapd  9120  div12apd  9121  div23apd  9122  divdirapd  9123  divsubdirapd  9124  div11apd  9125  ltmul12a  9154  ltdiv1  9162  ltrec  9177  lt2msq1  9179  lediv2  9185  lediv23  9187  recp1lt1  9193  qapne  9992  xadd4d  10240  xleaddadd  10242  modqge0  10721  modqlt  10722  modqid  10738  expgt1  10966  nnlesq  11032  expnbnd  11053  facubnd  11135  pfxsuffeqwrdeq  11418  resqrexlemover  11723  mulcn2  12025  cvgratnnlemnexp  12238  cvgratnnlemmn  12239  eftlub  12404  eflegeo  12415  sin01bnd  12471  cos01bnd  12472  eirraplem  12491  bitsmod  12670  bezoutlemnewy  12720  bezoutlemstep  12721  mulgcd  12740  mulgcddvds  12819  prmind2  12845  oddpwdclemxy  12894  oddpwdclemodd  12897  qnumgt0  12923  pcpremul  13019  fldivp1  13074  pcfaclem  13075  qexpz  13078  prmpwdvds  13081  pockthg  13083  4sqlem10  13113  4sqlem12  13128  4sqlem16  13132  4sqlem17  13133  ablsub4  14069  znrrg  14937  txdis  15271  txdis1cn  15272  xblm  15411  reeff1oleme  15766  tangtx  15832  cosordlem  15843  logdivlti  15875  apcxp2  15933  pellexlem2  15975  mersenne  15994  lgsdilem  16029  lgseisenlem1  16072  lgseisenlem2  16073  lgseisenlem3  16074  lgsquadlem1  16079  lgsquadlem2  16080  2sqlem3  16119  2sqlem8  16125  0uhgrsubgr  16389  eupth2lem3lem3fi  16594  apdifflemr  16970