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

Theorem an4s 578
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 576 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) ↔ ((𝜑𝜓) ∧ (𝜒𝜃)))
2 an4s.1 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
31, 2sylbi 120 1 (((𝜑𝜒) ∧ (𝜓𝜃)) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
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
This theorem is referenced by:  an42s  579  anandis  582  anandirs  583  trin2  4937  fnun  5236  2elresin  5241  f1co  5347  f1oun  5394  f1oco  5397  f1mpt  5679  poxp  6136  tfrlem7  6221  brecop  6526  th3qlem1  6538  oviec  6542  pmss12g  6576  addcmpblnq  7198  mulcmpblnq  7199  mulpipqqs  7204  mulclnq  7207  mulcanenq  7216  distrnqg  7218  mulcmpblnq0  7275  mulcanenq0ec  7276  mulclnq0  7283  nqnq0a  7285  nqnq0m  7286  distrnq0  7290  genipv  7340  genpelvl  7343  genpelvu  7344  genpml  7348  genpmu  7349  genpcdl  7350  genpcuu  7351  genprndl  7352  genprndu  7353  distrlem1prl  7413  distrlem1pru  7414  ltsopr  7427  addcmpblnr  7570  ltsrprg  7578  addclsr  7584  mulclsr  7585  addasssrg  7587  addresr  7668  mulresr  7669  axaddass  7703  axmulass  7704  axdistr  7705  mulgt0  7862  mul4  7917  add4  7946  2addsub  7999  addsubeq4  8000  sub4  8030  muladd  8169  mulsub  8186  add20i  8277  mulge0i  8405  mulap0b  8439  divmuldivap  8495  ltmul12a  8641  zmulcl  9130  uz2mulcl  9428  qaddcl  9453  qmulcl  9455  qreccl  9460  rpaddcl  9493  ge0addcl  9793  ge0xaddcl  9795  expge1  10360  rexanuz  10791  amgm2  10921  iooinsup  11077  mulcn2  11112  dvds2ln  11560  opoe  11626  omoe  11627  opeo  11628  omeo  11629  lcmgcd  11793  lcmdvds  11794  tgcl  12270  innei  12369  txbas  12464  txss12  12472  txbasval  12473  blsscls2  12699  qtopbasss  12727  bj-indind  13299
  Copyright terms: Public domain W3C validator