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

Theorem 3com12 1114
Description: Commutation in antecedent. Swap 1st and 2nd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3com12 ((𝜓𝜑𝜒) → 𝜃)

Proof of Theorem 3com12
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213exp 1109 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp21 1102 1 ((𝜓𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1071
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 199  df-an 387  df-3an 1073
This theorem is referenced by:  3comr  1116  3com23  1117  3adant2lOLD  1183  3adant2rOLD  1185  3imp21OLD  1406  brelrng  5601  fresaunres1  6327  fvun2  6530  onfununi  7721  oaword  7913  nnaword  7991  nnmword  7997  ecopovtrn  8134  fpmg  8166  tskord  9937  ltadd2  10480  mul12  10541  add12  10593  addsub  10634  addsubeq4  10638  ppncan  10665  leadd1  10843  ltaddsub2  10850  leaddsub2  10852  ltsub1  10871  ltsub2  10872  div23  11052  ltmul1  11227  ltmulgt11  11237  lediv1  11242  lemuldiv  11257  ltdiv2  11263  zdiv  11799  xltadd1  12398  xltmul1  12434  iooneg  12607  icoshft  12609  fzaddel  12692  fzshftral  12746  modmulmodr  13055  facwordi  13394  abssubge0  14474  climshftlem  14713  dvdsmul1  15410  divalglem8  15530  divalgb  15534  lcmgcdeq  15731  pcfac  16007  mhmmulg  17967  rmodislmodlem  19322  xrsdsreval  20187  cnmptcom  21890  hmeof1o2  21975  ordthmeo  22014  isclmi0  23305  iscvsi  23336  cxplt2  24881  axcontlem8  26320  vcdi  27992  isvciOLD  28007  dipdi  28270  dipsubdi  28276  hvadd12  28464  hvmulcom  28472  his5  28515  bcs3  28612  chj12  28965  spansnmul  28995  homul12  29236  hoaddsub  29247  lnopmul  29398  lnopaddmuli  29404  lnopsubmuli  29406  lnfnaddmuli  29476  leop2  29555  dmdsl3  29746  chirredlem3  29823  atmd2  29831  cdj3lem3  29869  signstfvc  31252  3com12d  32893  cnambfre  34067  sdclem2  34146  addrcom  39615  uun123p1  39960  sineq0ALT  40088  stoweidlem17  41143  sigaras  41953  sigarms  41954
  Copyright terms: Public domain W3C validator