Theorem an4s 596

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 592	. 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  597  anandis  600  anandirs  601  trin2  5174  fnun  5484  2elresin  5489  f1co  5605  f1oun  5654  f1oco  5657  f1mpt  5967  poxp  6458  tfrlem7  6578  brecop  6889  th3qlem1  6901  oviec  6905  pmss12g  6946  addcmpblnq  7724  mulcmpblnq  7725  mulpipqqs  7730  mulclnq  7733  mulcanenq  7742  distrnqg  7744  mulcmpblnq0  7801  mulcanenq0ec  7802  mulclnq0  7809  nqnq0a  7811  nqnq0m  7812  distrnq0  7816  genipv  7866  genpelvl  7869  genpelvu  7870  genpml  7874  genpmu  7875  genpcdl  7876  genpcuu  7877  genprndl  7878  genprndu  7879  distrlem1prl  7939  distrlem1pru  7940  ltsopr  7953  addcmpblnr  8096  ltsrprg  8104  addclsr  8110  mulclsr  8111  addasssrg  8113  addresr  8194  mulresr  8195  axaddass  8229  axmulass  8230  axdistr  8231  mulgt0  8390  mul4  8448  add4  8477  2addsub  8530  addsubeq4  8531  sub4  8561  muladd  8701  mulsub  8718  add20i  8810  mulge0i  8938  mulap0b  8973  divmuldivap  9032  ltmul12a  9180  zmulcl  9677  uz2mulcl  9987  qaddcl  10014  qmulcl  10016  qreccl  10021  rpaddcl  10057  ge0addcl  10362  ge0xaddcl  10364  expge1  10991  rexanuz  11732  amgm2  11862  iooinsup  12021  mulcn2  12056  dvds2ln  12569  opoe  12640  omoe  12641  opeo  12642  omeo  12643  lcmgcd  12834  lcmdvds  12835  pc2dvds  13087  tgcl  15088  innei  15187  txbas  15282  txss12  15290  txbasval  15291  blsscls2  15517  qtopbasss  15545  lgslem3  16035  bj-indind  16872