ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3jca GIF version

Theorem 3jca 1119
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 302 . 2 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
5 df-3an 922 . 2 ((𝜓𝜒𝜃) ↔ ((𝜓𝜒) ∧ 𝜃))
64, 5sylibr 132 1 (𝜑 → (𝜓𝜒𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  3jcad  1120  mpbir3and  1122  syl3anbrc  1123  3anim123i  1124  syl3anc  1170  syl13anc  1172  syl31anc  1173  syl113anc  1182  syl131anc  1183  syl311anc  1184  syl33anc  1185  syl133anc  1193  syl313anc  1194  syl331anc  1195  syl333anc  1202  3jaob  1234  mp3and  1272  issod  4082  tfrlemibxssdm  5976  tfr1onlembxssdm  5992  tfrcllembxssdm  6005  ltexnqq  6660  enq0tr  6686  prarloc  6755  addclpr  6789  nqprxx  6798  mulclpr  6824  ltexprlempr  6860  recexprlempr  6884  cauappcvgprlemcl  6905  caucvgprlemcl  6928  caucvgprprlemcl  6956  le2tri3i  7286  ltmul1  7759  nn0ge2m1nn  8415  nn0ge0div  8515  eluzp1p1  8725  peano2uz  8752  ledivge1le  8884  elioc2  9035  elico2  9036  elicc2  9037  iccsupr  9065  uzsubsubfz  9142  fzrev3  9180  elfz1b  9183  fseq1p1m1  9187  elfz0ubfz0  9213  elfz0fzfz0  9214  fz0fzelfz0  9215  fz0fzdiffz0  9218  elfzmlbp  9220  elfzo2  9237  elfzo0  9268  fzo1fzo0n0  9269  elfzo0z  9270  fzofzim  9274  elfzo1  9276  ubmelfzo  9286  elfzodifsumelfzo  9287  elfzom1elp1fzo  9288  fzossfzop1  9298  ssfzo12bi  9311  subfzo0  9328  fldiv4p1lem1div2  9387  intqfrac2  9401  intfracq  9402  modfzo0difsn  9477  remullem  9896  qdenre  10226  maxabslemval  10232  divconjdvds  10394  addmodlteqALT  10404  ltoddhalfle  10437  4dvdseven  10461  dfgcd2  10547  rppwr  10561  qredeq  10622  divgcdcoprmex  10628  cncongr1  10629  dvdsnprmd  10651  oddprmge3  10660
  Copyright terms: Public domain W3C validator