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

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
StepHypRef Expression
1 sylXanc.1 . 2 (𝜑𝜓)
2 sylXanc.2 . 2 (𝜑𝜒)
3 sylXanc.3 . . 3 (𝜑𝜃)
4 sylXanc.4 . . 3 (𝜑𝜏)
53, 4jca 304 . 2 (𝜑 → (𝜃𝜏))
6 syl112anc.5 . 2 ((𝜓𝜒 ∧ (𝜃𝜏)) → 𝜂)
71, 2, 5, 6syl3anc 1217 1 (𝜑𝜂)
 Colors of variables: wff set class 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  5496  caseinl  6986  caseinr  6987  reapmul1  8401  recrecap  8513  rec11rap  8515  divdivdivap  8517  dmdcanap  8526  ddcanap  8530  rerecclap  8534  div2negap  8539  divap1d  8605  divmulapd  8616  apdivmuld  8617  divmulap2d  8628  divmulap3d  8629  divassapd  8630  div12apd  8631  div23apd  8632  divdirapd  8633  divsubdirapd  8634  div11apd  8635  ltmul12a  8662  ltdiv1  8670  ltrec  8685  lt2msq1  8687  lediv2  8693  lediv23  8695  recp1lt1  8701  qapne  9478  xadd4d  9718  xleaddadd  9720  modqge0  10156  modqlt  10157  modqid  10173  expgt1  10382  nnlesq  10447  expnbnd  10466  facubnd  10543  resqrexlemover  10834  mulcn2  11133  cvgratnnlemnexp  11345  cvgratnnlemmn  11346  eftlub  11453  eflegeo  11464  sin01bnd  11520  cos01bnd  11521  eirraplem  11539  bezoutlemnewy  11740  bezoutlemstep  11741  mulgcd  11760  mulgcddvds  11831  prmind2  11857  oddpwdclemxy  11903  oddpwdclemodd  11906  qnumgt0  11932  txdis  12505  txdis1cn  12506  xblm  12645  reeff1oleme  12921  tangtx  12987  cosordlem  12998  logdivlti  13030  apcxp2  13086  apdifflemr  13436
 Copyright terms: Public domain W3C validator