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  5745  caseinl  7384  caseinr  7385  reapmul1  8874  recrecap  8988  rec11rap  8990  divdivdivap  8992  dmdcanap  9001  ddcanap  9005  rerecclap  9009  div2negap  9014  divap1d  9080  divmulapd  9091  apdivmuld  9092  divmulap2d  9103  divmulap3d  9104  divassapd  9105  div12apd  9106  div23apd  9107  divdirapd  9108  divsubdirapd  9109  div11apd  9110  ltmul12a  9139  ltdiv1  9147  ltrec  9162  lt2msq1  9164  lediv2  9170  lediv23  9172  recp1lt1  9178  qapne  9977  xadd4d  10224  xleaddadd  10226  modqge0  10701  modqlt  10702  modqid  10718  expgt1  10946  nnlesq  11012  expnbnd  11033  facubnd  11115  pfxsuffeqwrdeq  11398  resqrexlemover  11703  mulcn2  12005  cvgratnnlemnexp  12218  cvgratnnlemmn  12219  eftlub  12384  eflegeo  12395  sin01bnd  12451  cos01bnd  12452  eirraplem  12471  bitsmod  12650  bezoutlemnewy  12700  bezoutlemstep  12701  mulgcd  12720  mulgcddvds  12799  prmind2  12825  oddpwdclemxy  12874  oddpwdclemodd  12877  qnumgt0  12903  pcpremul  12999  fldivp1  13054  pcfaclem  13055  qexpz  13058  prmpwdvds  13061  pockthg  13063  4sqlem10  13093  4sqlem12  13108  4sqlem16  13112  4sqlem17  13113  ablsub4  14051  znrrg  14857  txdis  15191  txdis1cn  15192  xblm  15331  reeff1oleme  15686  tangtx  15752  cosordlem  15763  logdivlti  15795  apcxp2  15853  pellexlem2  15895  mersenne  15914  lgsdilem  15949  lgseisenlem1  15992  lgseisenlem2  15993  lgseisenlem3  15994  lgsquadlem1  15999  lgsquadlem2  16000  2sqlem3  16039  2sqlem8  16045  0uhgrsubgr  16309  eupth2lem3lem3fi  16514  apdifflemr  16880