MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nanbi12d Unicode version

Theorem nanbi12d 1309
Description: Join two logical equivalences with anti-conjunction. (Contributed by Scott Fenton, 2-Jan-2018.)
Hypotheses
Ref Expression
nanbid.1  |-  ( ph  ->  ( ps  <->  ch )
)
nanbi12d.2  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
nanbi12d  |-  ( ph  ->  ( ( ps  -/\  th )  <->  ( ch  -/\  ta ) ) )

Proof of Theorem nanbi12d
StepHypRef Expression
1 nanbid.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 nanbi12d.2 . 2  |-  ( ph  ->  ( th  <->  ta )
)
3 nanbi12 1303 . 2  |-  ( ( ( ps  <->  ch )  /\  ( th  <->  ta )
)  ->  ( ( ps  -/\  th )  <->  ( ch  -/\ 
ta ) ) )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( ( ps  -/\  th )  <->  ( ch  -/\  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    -/\ wnan 1293
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-nan 1294
  Copyright terms: Public domain W3C validator