New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  3jca GIF version

Theorem 3jca 1132
 Description: Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
Hypotheses
Ref Expression
3jca.1 (φψ)
3jca.2 (φχ)
3jca.3 (φθ)
Assertion
Ref Expression
3jca (φ → (ψ χ θ))

Proof of Theorem 3jca
StepHypRef Expression
1 3jca.1 . . 3 (φψ)
2 3jca.2 . . 3 (φχ)
3 3jca.3 . . 3 (φθ)
41, 2, 3jca31 520 . 2 (φ → ((ψ χ) θ))
5 df-3an 936 . 2 ((ψ χ θ) ↔ ((ψ χ) θ))
64, 5sylibr 203 1 (φ → (ψ χ θ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358   ∧ w3a 934 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936 This theorem is referenced by:  3jcad  1133  mpbir3and  1135  syl3anbrc  1136  3anim123i  1137  syl3anc  1182  syl13anc  1184  syl31anc  1185  syl113anc  1194  syl131anc  1195  syl311anc  1196  syl33anc  1197  syl133anc  1205  syl313anc  1206  syl331anc  1207  syl333anc  1214  3jaob  1244  mp3and  1280  1cvsfin  4542
 Copyright terms: Public domain W3C validator