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

Theorem an4s 530
Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
Hypothesis
Ref Expression
an4s.1 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
Assertion
Ref Expression
an4s (((𝜑𝜒) ∧ (𝜓𝜃)) → 𝜏)

Proof of Theorem an4s
StepHypRef Expression
1 an4 528 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) ↔ ((𝜑𝜓) ∧ (𝜒𝜃)))
2 an4s.1 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
31, 2sylbi 118 1 (((𝜑𝜒) ∧ (𝜓𝜃)) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  an42s  531  anandis  534  anandirs  535  trin2  4741  fnun  5030  2elresin  5035  f1co  5126  f1oun  5171  f1oco  5174  f1mpt  5435  poxp  5878  tfrlem7  5961  brecop  6224  th3qlem1  6236  oviec  6240  addcmpblnq  6493  mulcmpblnq  6494  mulpipqqs  6499  mulclnq  6502  mulcanenq  6511  distrnqg  6513  mulcmpblnq0  6570  mulcanenq0ec  6571  mulclnq0  6578  nqnq0a  6580  nqnq0m  6581  distrnq0  6585  genipv  6635  genpelvl  6638  genpelvu  6639  genpml  6643  genpmu  6644  genpcdl  6645  genpcuu  6646  genprndl  6647  genprndu  6648  distrlem1prl  6708  distrlem1pru  6709  ltsopr  6722  addcmpblnr  6852  ltsrprg  6860  addclsr  6866  mulclsr  6867  addasssrg  6869  addresr  6941  mulresr  6942  axaddass  6974  axmulass  6975  axdistr  6976  mulgt0  7122  mul4  7176  add4  7205  2addsub  7258  addsubeq4  7259  sub4  7289  muladd  7423  mulsub  7440  add20i  7528  mulge0i  7655  mulap0b  7680  divmuldivap  7733  ltmul12a  7871  zmulcl  8325  uz2mulcl  8612  qaddcl  8637  qmulcl  8639  qreccl  8644  rpaddcl  8674  ge0addcl  8921  serige0  9382  expge1  9422  rexanuz  9779  amgm2  9908  mulcn2  10027  dvds2ln  10103  opoe  10170  omoe  10171  opeo  10172  omeo  10173  bj-indind  10386
  Copyright terms: Public domain W3C validator