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

Theorem 3anim123i 1240
 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 1075 . 2 ((𝜑𝜒𝜏) → 𝜓)
3 3anim123i.2 . . 3 (𝜒𝜃)
433ad2ant2 1076 . 2 ((𝜑𝜒𝜏) → 𝜃)
5 3anim123i.3 . . 3 (𝜏𝜂)
653ad2ant3 1077 . 2 ((𝜑𝜒𝜏) → 𝜂)
72, 4, 63jca 1235 1 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  3anim1i  1241  3anim2i  1242  3anim3i  1243  syl3an  1360  syl3anl  1369  spc3egv  3270  eloprabga  6645  le2tri3i  10046  fzmmmeqm  12245  elfz1b  12279  elfz0fzfz0  12313  elfzmlbp  12319  elfzo1  12385  ssfzoulel  12428  flltdivnn0lt  12496  swrdswrd  13312  swrdccatin2  13338  swrdccat  13344  modmulconst  14851  mulmoddvds  14889  nndvdslegcd  15065  ncoprmlnprm  15274  symg2hash  17640  pmtrdifellem2  17720  unitgrp  18490  isdrngd  18595  bcthlem5  22933  lgsmulsqcoprm  24868  colinearalg  25590  axcontlem8  25651  usgra2adedgwlk  26142  chirredlem2  28634  rexdiv  28965  bnj944  30262  bnj969  30270  nnssi2  31624  nnssi3  31625  isdrngo2  32927  leatb  33597  paddasslem9  34132  paddasslem10  34133  dvhvaddass  35404  expgrowthi  37554  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  cplgr3v  40657  21wlkdlem3  41134  umgr2adedgwlk  41152  elwwlks2  41170  31wlkdlem5  41330  31wlkdlem6  41332  31wlkdlem7  41333  31wlkdlem8  41334  2zrngasgrp  41730  2zrngmsgrp  41737  lincvalpr  42001  refdivmptf  42134  refdivmptfv  42138
 Copyright terms: Public domain W3C validator