Theorem nxtand 14313

Description: (ph /\ ps) holds in the next step iff ph holds in the next step and ps holds in the next step. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)

Assertion

Ref	Expression
nxtand	|- (()(ph /\ ps) <-> (()ph /\ ()ps))

Proof of Theorem nxtand

Step	Hyp	Ref	Expression
1		simpl 346	. . . 4 |- ((ph /\ ps) -> ph)
2	1	impxt 14310	. . 3 |- (()(ph /\ ps) -> ()ph)
3		simpr 350	. . . 4 |- ((ph /\ ps) -> ps)
4	3	impxt 14310	. . 3 |- (()(ph /\ ps) -> ()ps)
5	2, 4	jca 310	. 2 |- (()(ph /\ ps) -> (()ph /\ ()ps))
6		pm3.2 305	. . . . 5 |- (ph -> (ps -> (ph /\ ps)))
7	6	impxt 14310	. . . 4 |- (()ph -> ()(ps -> (ph /\ ps)))
8		ax-ltl3 14303	. . . 4 |- (()(ps -> (ph /\ ps)) -> (()ps -> ()(ph /\ ps)))
9	7, 8	syl 12	. . 3 |- (()ph -> (()ps -> ()(ph /\ ps)))
10	9	imp 377	. 2 |- ((()ph /\ ()ps) -> ()(ph /\ ps))
11	5, 10	impbii 174	1 |- (()(ph /\ ps) <-> (()ph /\ ()ps))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  ()wcirc 14299

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-ltl3 14303  ax-nmp 14306

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain