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

Theorem an4s 553
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 551 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) ↔ ((𝜑𝜓) ∧ (𝜒𝜃)))
2 an4s.1 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
31, 2sylbi 119 1 (((𝜑𝜒) ∧ (𝜓𝜃)) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  an42s  554  anandis  557  anandirs  558  trin2  4766  fnun  5056  2elresin  5061  f1co  5152  f1oun  5197  f1oco  5200  f1mpt  5462  poxp  5904  tfrlem7  5986  brecop  6283  th3qlem1  6295  oviec  6299  addcmpblnq  6671  mulcmpblnq  6672  mulpipqqs  6677  mulclnq  6680  mulcanenq  6689  distrnqg  6691  mulcmpblnq0  6748  mulcanenq0ec  6749  mulclnq0  6756  nqnq0a  6758  nqnq0m  6759  distrnq0  6763  genipv  6813  genpelvl  6816  genpelvu  6817  genpml  6821  genpmu  6822  genpcdl  6823  genpcuu  6824  genprndl  6825  genprndu  6826  distrlem1prl  6886  distrlem1pru  6887  ltsopr  6900  addcmpblnr  7030  ltsrprg  7038  addclsr  7044  mulclsr  7045  addasssrg  7047  addresr  7119  mulresr  7120  axaddass  7152  axmulass  7153  axdistr  7154  mulgt0  7305  mul4  7359  add4  7388  2addsub  7441  addsubeq4  7442  sub4  7472  muladd  7607  mulsub  7624  add20i  7712  mulge0i  7839  mulap0b  7864  divmuldivap  7919  ltmul12a  8057  zmulcl  8537  uz2mulcl  8828  qaddcl  8853  qmulcl  8855  qreccl  8860  rpaddcl  8890  ge0addcl  9132  serige0  9622  expge1  9662  rexanuz  10075  amgm2  10205  mulcn2  10352  dvds2ln  10436  opoe  10502  omoe  10503  opeo  10504  omeo  10505  lcmgcd  10667  lcmdvds  10668  bj-indind  10994
  Copyright terms: Public domain W3C validator