ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl112anc GIF version

Theorem syl112anc 1203
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
StepHypRef Expression
1 sylXanc.1 . 2 (𝜑𝜓)
2 sylXanc.2 . 2 (𝜑𝜒)
3 sylXanc.3 . . 3 (𝜑𝜃)
4 sylXanc.4 . . 3 (𝜑𝜏)
53, 4jca 302 . 2 (𝜑 → (𝜃𝜏))
6 syl112anc.5 . 2 ((𝜓𝜒 ∧ (𝜃𝜏)) → 𝜂)
71, 2, 5, 6syl3anc 1199 1 (𝜑𝜂)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 945
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 947
This theorem is referenced by:  fvun1  5453  caseinl  6942  caseinr  6943  reapmul1  8320  recrecap  8429  rec11rap  8431  divdivdivap  8433  dmdcanap  8442  ddcanap  8446  rerecclap  8450  div2negap  8455  divap1d  8521  divmulapd  8532  apdivmuld  8533  divmulap2d  8544  divmulap3d  8545  divassapd  8546  div12apd  8547  div23apd  8548  divdirapd  8549  divsubdirapd  8550  div11apd  8551  ltmul12a  8575  ltdiv1  8583  ltrec  8598  lt2msq1  8600  lediv2  8606  lediv23  8608  recp1lt1  8614  qapne  9380  xadd4d  9608  xleaddadd  9610  modqge0  10045  modqlt  10046  modqid  10062  expgt1  10271  nnlesq  10336  expnbnd  10355  facubnd  10431  resqrexlemover  10722  mulcn2  11021  cvgratnnlemnexp  11233  cvgratnnlemmn  11234  eftlub  11295  eflegeo  11307  sin01bnd  11363  cos01bnd  11364  eirraplem  11379  bezoutlemnewy  11580  bezoutlemstep  11581  mulgcd  11600  mulgcddvds  11671  prmind2  11697  oddpwdclemxy  11742  oddpwdclemodd  11745  qnumgt0  11771  txdis  12341  txdis1cn  12342  xblm  12481
  Copyright terms: Public domain W3C validator