Theorem syl112anc 1242

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

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

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 980

This theorem is referenced by:  fvun1  5582  caseinl  7089  caseinr  7090  reapmul1  8551  recrecap  8665  rec11rap  8667  divdivdivap  8669  dmdcanap  8678  ddcanap  8682  rerecclap  8686  div2negap  8691  divap1d  8757  divmulapd  8768  apdivmuld  8769  divmulap2d  8780  divmulap3d  8781  divassapd  8782  div12apd  8783  div23apd  8784  divdirapd  8785  divsubdirapd  8786  div11apd  8787  ltmul12a  8816  ltdiv1  8824  ltrec  8839  lt2msq1  8841  lediv2  8847  lediv23  8849  recp1lt1  8855  qapne  9638  xadd4d  9884  xleaddadd  9886  modqge0  10331  modqlt  10332  modqid  10348  expgt1  10557  nnlesq  10623  expnbnd  10643  facubnd  10724  resqrexlemover  11018  mulcn2  11319  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  eftlub  11697  eflegeo  11708  sin01bnd  11764  cos01bnd  11765  eirraplem  11783  bezoutlemnewy  11996  bezoutlemstep  11997  mulgcd  12016  mulgcddvds  12093  prmind2  12119  oddpwdclemxy  12168  oddpwdclemodd  12171  qnumgt0  12197  pcpremul  12292  fldivp1  12345  pcfaclem  12346  qexpz  12349  prmpwdvds  12352  pockthg  12354  4sqlem10  12384  ablsub4  13114  txdis  13747  txdis1cn  13748  xblm  13887  reeff1oleme  14163  tangtx  14229  cosordlem  14240  logdivlti  14272  apcxp2  14328  lgsdilem  14398  lgseisenlem1  14420  lgseisenlem2  14421  2sqlem3  14434  2sqlem8  14440  apdifflemr  14765