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  5574  caseinl  7080  caseinr  7081  reapmul1  8526  recrecap  8638  rec11rap  8640  divdivdivap  8642  dmdcanap  8651  ddcanap  8655  rerecclap  8659  div2negap  8664  divap1d  8730  divmulapd  8741  apdivmuld  8742  divmulap2d  8753  divmulap3d  8754  divassapd  8755  div12apd  8756  div23apd  8757  divdirapd  8758  divsubdirapd  8759  div11apd  8760  ltmul12a  8788  ltdiv1  8796  ltrec  8811  lt2msq1  8813  lediv2  8819  lediv23  8821  recp1lt1  8827  qapne  9610  xadd4d  9854  xleaddadd  9856  modqge0  10300  modqlt  10301  modqid  10317  expgt1  10526  nnlesq  10591  expnbnd  10611  facubnd  10691  resqrexlemover  10985  mulcn2  11286  cvgratnnlemnexp  11498  cvgratnnlemmn  11499  eftlub  11664  eflegeo  11675  sin01bnd  11731  cos01bnd  11732  eirraplem  11750  bezoutlemnewy  11962  bezoutlemstep  11963  mulgcd  11982  mulgcddvds  12059  prmind2  12085  oddpwdclemxy  12134  oddpwdclemodd  12137  qnumgt0  12163  pcpremul  12258  fldivp1  12311  pcfaclem  12312  qexpz  12315  prmpwdvds  12318  pockthg  12320  4sqlem10  12350  ablsub4  12912  txdis  13328  txdis1cn  13329  xblm  13468  reeff1oleme  13744  tangtx  13810  cosordlem  13821  logdivlti  13853  apcxp2  13909  lgsdilem  13979  2sqlem3  14004  2sqlem8  14010  apdifflemr  14336