Theorem syl112anc 1221

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 304	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏))
6		syl112anc.5	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	1, 2, 5, 6	syl3anc 1217	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  fvun1  5495  caseinl  6984  caseinr  6985  reapmul1  8381  recrecap  8493  rec11rap  8495  divdivdivap  8497  dmdcanap  8506  ddcanap  8510  rerecclap  8514  div2negap  8519  divap1d  8585  divmulapd  8596  apdivmuld  8597  divmulap2d  8608  divmulap3d  8609  divassapd  8610  div12apd  8611  div23apd  8612  divdirapd  8613  divsubdirapd  8614  div11apd  8615  ltmul12a  8642  ltdiv1  8650  ltrec  8665  lt2msq1  8667  lediv2  8673  lediv23  8675  recp1lt1  8681  qapne  9458  xadd4d  9698  xleaddadd  9700  modqge0  10136  modqlt  10137  modqid  10153  expgt1  10362  nnlesq  10427  expnbnd  10446  facubnd  10523  resqrexlemover  10814  mulcn2  11113  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  eftlub  11433  eflegeo  11444  sin01bnd  11500  cos01bnd  11501  eirraplem  11519  bezoutlemnewy  11720  bezoutlemstep  11721  mulgcd  11740  mulgcddvds  11811  prmind2  11837  oddpwdclemxy  11883  oddpwdclemodd  11886  qnumgt0  11912  txdis  12485  txdis1cn  12486  xblm  12625  reeff1oleme  12901  tangtx  12967  cosordlem  12978  logdivlti  13010  apcxp2  13066  apdifflemr  13415