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  5120  fnun  5429  2elresin  5434  f1co  5545  f1oun  5594  f1oco  5597  f1mpt  5901  poxp  6384  tfrlem7  6469  brecop  6780  th3qlem1  6792  oviec  6796  pmss12g  6830  addcmpblnq  7565  mulcmpblnq  7566  mulpipqqs  7571  mulclnq  7574  mulcanenq  7583  distrnqg  7585  mulcmpblnq0  7642  mulcanenq0ec  7643  mulclnq0  7650  nqnq0a  7652  nqnq0m  7653  distrnq0  7657  genipv  7707  genpelvl  7710  genpelvu  7711  genpml  7715  genpmu  7716  genpcdl  7717  genpcuu  7718  genprndl  7719  genprndu  7720  distrlem1prl  7780  distrlem1pru  7781  ltsopr  7794  addcmpblnr  7937  ltsrprg  7945  addclsr  7951  mulclsr  7952  addasssrg  7954  addresr  8035  mulresr  8036  axaddass  8070  axmulass  8071  axdistr  8072  mulgt0  8232  mul4  8289  add4  8318  2addsub  8371  addsubeq4  8372  sub4  8402  muladd  8541  mulsub  8558  add20i  8650  mulge0i  8778  mulap0b  8813  divmuldivap  8870  ltmul12a  9018  zmulcl  9511  uz2mulcl  9815  qaddcl  9842  qmulcl  9844  qreccl  9849  rpaddcl  9885  ge0addcl  10189  ge0xaddcl  10191  expge1  10810  rexanuz  11514  amgm2  11644  iooinsup  11803  mulcn2  11838  dvds2ln  12350  opoe  12421  omoe  12422  opeo  12423  omeo  12424  lcmgcd  12615  lcmdvds  12616  pc2dvds  12868  tgcl  14753  innei  14852  txbas  14947  txss12  14955  txbasval  14956  blsscls2  15182  qtopbasss  15210  lgslem3  15696  bj-indind  16350