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

Theorem 3anim123i 1148
 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 1130 . 2 ((𝜑𝜒𝜏) → 𝜓)
3 3anim123i.2 . . 3 (𝜒𝜃)
433ad2ant2 1131 . 2 ((𝜑𝜒𝜏) → 𝜃)
5 3anim123i.3 . . 3 (𝜏𝜂)
653ad2ant3 1132 . 2 ((𝜑𝜒𝜏) → 𝜂)
72, 4, 63jca 1125 1 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  3anim1i  1149  3anim2i  1150  3anim3i  1151  syl3an  1157  syl3anl  1412  eloprabga  7241  le2tri3i  10762  fzmmmeqm  12938  elfz0fzfz0  13010  elfzmlbp  13016  elfzo1  13085  ssfzoulel  13129  flltdivnn0lt  13201  pfxeq  14052  swrdswrd  14061  swrdccat  14091  modmulconst  15636  nndvdslegcd  15847  ncoprmlnprm  16061  setsstruct2  16516  efmnd2hash  18054  symg2hash  18516  pmtrdifellem2  18601  unitgrp  19417  isdrngd  19524  bcthlem5  23942  lgsmulsqcoprm  25937  colinearalg  26714  axcontlem8  26775  cplgr3v  27235  2wlkdlem3  27723  umgr2adedgwlk  27741  elwwlks2  27762  clwwlkinwwlk  27835  3wlkdlem5  27958  3wlkdlem6  27960  3wlkdlem7  27961  3wlkdlem8  27962  numclwwlk1lem2foalem  28146  chirredlem2  30184  rexdiv  30638  bnj944  32335  bnj969  32343  nnssi2  33931  nnssi3  33932  isdrngo2  35415  leatb  36607  paddasslem9  37143  paddasslem10  37144  dvhvaddass  38412  expgrowthi  41080  elsetpreimafveq  43957  nnsum4primesodd  44357  nnsum4primesoddALTV  44358  nn0mnd  44482  2zrngasgrp  44607  2zrngmsgrp  44614  mapprop  44791  lincvalpr  44868  refdivmptf  44997  refdivmptfv  45001  itsclc0yqsollem2  45218
 Copyright terms: Public domain W3C validator