MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anim123i Structured version   Visualization version   GIF version

Theorem 3anim123i 1266
Description: Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.)
Hypotheses
Ref Expression
3anim123i.1 (𝜑𝜓)
3anim123i.2 (𝜒𝜃)
3anim123i.3 (𝜏𝜂)
Assertion
Ref Expression
3anim123i ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))

Proof of Theorem 3anim123i
StepHypRef Expression
1 3anim123i.1 . . 3 (𝜑𝜓)
213ad2ant1 1102 . 2 ((𝜑𝜒𝜏) → 𝜓)
3 3anim123i.2 . . 3 (𝜒𝜃)
433ad2ant2 1103 . 2 ((𝜑𝜒𝜏) → 𝜃)
5 3anim123i.3 . . 3 (𝜏𝜂)
653ad2ant3 1104 . 2 ((𝜑𝜒𝜏) → 𝜂)
72, 4, 63jca 1261 1 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  3anim1i  1267  3anim2i  1268  3anim3i  1269  syl3an  1408  syl3anl  1417  spc3egv  3328  eloprabga  6789  le2tri3i  10205  fzmmmeqm  12412  elfz0fzfz0  12483  elfzmlbp  12489  elfzo1  12557  ssfzoulel  12602  flltdivnn0lt  12674  swrdswrd  13506  swrdccatin2  13533  swrdccat  13539  modmulconst  15060  nndvdslegcd  15274  ncoprmlnprm  15483  setsstruct2  15943  symg2hash  17863  pmtrdifellem2  17943  unitgrp  18713  isdrngd  18820  bcthlem5  23171  lgsmulsqcoprm  25113  colinearalg  25835  axcontlem8  25896  cplgr3v  26387  2wlkdlem3  26892  umgr2adedgwlk  26910  elwwlks2  26933  clwwlkinwwlk  27003  3wlkdlem5  27141  3wlkdlem6  27143  3wlkdlem7  27144  3wlkdlem8  27145  numclwlk1lem2foalem  27341  chirredlem2  29378  rexdiv  29762  bnj944  31134  bnj969  31142  nnssi2  32579  nnssi3  32580  isdrngo2  33887  leatb  34897  paddasslem9  35432  paddasslem10  35433  dvhvaddass  36703  expgrowthi  38849  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  2zrngasgrp  42265  2zrngmsgrp  42272  lincvalpr  42532  refdivmptf  42661  refdivmptfv  42665
  Copyright terms: Public domain W3C validator