Theorem an4s 590

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

Step	Hyp	Ref	Expression
1		an4 586	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)))
2		an4s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
3	1, 2	sylbi 121	1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  an42s  591  anandis  594  anandirs  595  trin2  5126  fnun  5435  2elresin  5440  f1co  5551  f1oun  5600  f1oco  5603  f1mpt  5907  poxp  6392  tfrlem7  6478  brecop  6789  th3qlem1  6801  oviec  6805  pmss12g  6839  addcmpblnq  7577  mulcmpblnq  7578  mulpipqqs  7583  mulclnq  7586  mulcanenq  7595  distrnqg  7597  mulcmpblnq0  7654  mulcanenq0ec  7655  mulclnq0  7662  nqnq0a  7664  nqnq0m  7665  distrnq0  7669  genipv  7719  genpelvl  7722  genpelvu  7723  genpml  7727  genpmu  7728  genpcdl  7729  genpcuu  7730  genprndl  7731  genprndu  7732  distrlem1prl  7792  distrlem1pru  7793  ltsopr  7806  addcmpblnr  7949  ltsrprg  7957  addclsr  7963  mulclsr  7964  addasssrg  7966  addresr  8047  mulresr  8048  axaddass  8082  axmulass  8083  axdistr  8084  mulgt0  8244  mul4  8301  add4  8330  2addsub  8383  addsubeq4  8384  sub4  8414  muladd  8553  mulsub  8570  add20i  8662  mulge0i  8790  mulap0b  8825  divmuldivap  8882  ltmul12a  9030  zmulcl  9523  uz2mulcl  9832  qaddcl  9859  qmulcl  9861  qreccl  9866  rpaddcl  9902  ge0addcl  10206  ge0xaddcl  10208  expge1  10828  rexanuz  11539  amgm2  11669  iooinsup  11828  mulcn2  11863  dvds2ln  12375  opoe  12446  omoe  12447  opeo  12448  omeo  12449  lcmgcd  12640  lcmdvds  12641  pc2dvds  12893  tgcl  14778  innei  14877  txbas  14972  txss12  14980  txbasval  14981  blsscls2  15207  qtopbasss  15235  lgslem3  15721  bj-indind  16463